Automated Lean Proofs for Every Type (galois.com)

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.

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

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