[HN Gopher] Automated Lean Proofs for Every Type
       ___________________________________________________________________
        
       Automated Lean Proofs for Every Type
        
       Author : surprisetalk
       Score  : 36 points
       Date   : 2025-10-06 10:19 UTC (4 days ago)
        
 (HTM) web link (www.galois.com)
 (TXT) w3m dump (www.galois.com)
        
       | crvdgc wrote:
       | 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 wrote:
         | same
        
       | docandrew wrote:
       | Feels like maybe this is retreading ground covered by Why3ML, but
       | perhaps I'm missing something.
       | 
       | https://www.why3.org/doc/whyml.html
        
       ___________________________________________________________________
       (page generated 2025-10-10 23:02 UTC)