crvdgc 2 days ago 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. ProofHouse 2 days ago same
docandrew 2 days ago Feels like maybe this is retreading ground covered by Why3ML, but perhaps I’m missing something.https://www.why3.org/doc/whyml.html lgas 2 days ago Presumably this is aimed at people that want to take advantage of it in Lean.
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.
same
Feels like maybe this is retreading ground covered by Why3ML, but perhaps I’m missing something.
https://www.why3.org/doc/whyml.html
Presumably this is aimed at people that want to take advantage of it in Lean.