Automated Lean Proofs for Every Type

 (galois.com)

40 points | by surprisetalk 4 days ago

2 comments

  • docandrew 9 hours 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 1 hour ago
      Presumably this is aimed at people that want to take advantage of it in Lean.
  • crvdgc 20 hours 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.
    [-]