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.