3 ms·
Automated Lean Proofs for Every Type
- crvdgc 1y agoFrom the title I thought they solved math! Turns out to be a framework to use SMT solvers for decision-based proof. For additional types, you still need to write the bridging part. Interesting nonetheless.
- ProofHouse 1y agosame
- docandrew 1y agoFeels like maybe this is retreading ground covered by Why3ML, but perhaps I’m missing something. https://www.why3.org/doc/whyml.html https://www.why3.org/doc/whyml.html
- lgas 1y agoPresumably this is aimed at people that want to take advantage of it in Lean.