Automated Lean Proofs for Every Type(galois.com)

40 pointsby surprisetalk9 mesi fa4 comments

https://www.galois.com/articles/automated-lean-proofs-for-every-type

4 comments

crvdgc9 mesi fa

From 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.

ProofHouse9 mesi fa

same

docandrew9 mesi fa

Feels like maybe this is retreading ground covered by Why3ML, but perhaps I’m missing something.

https://www.why3.org/doc/whyml.html

lgas9 mesi fa

Presumably this is aimed at people that want to take advantage of it in Lean.