[HN Gopher] Discharging Lean goals into SMT solvers
       ___________________________________________________________________
        
       Discharging Lean goals into SMT solvers
        
       Author : ndrwnaguib
       Score  : 46 points
       Date   : 2024-11-21 20:02 UTC (1 days ago)
        
 (HTM) web link (github.com)
 (TXT) w3m dump (github.com)
        
       | benchmarkist wrote:
       | Similar to sledgehammer in Isabelle/HOL.
        
         | robinzfc wrote:
         | A bit of history: Sledgehammer became fully operational in
         | 2007, extended to call external SMT solvers in 2008. Looks like
         | Lean is catching up.
        
           | GregarianChild wrote:
           | That remains to be seen.
           | 
           | SMT solvers such as Z3 and CVC5 tend to be good at theory
           | solving (the T in SMT) but not so good at handling
           | quantification. OTOH, the ATPs (= automatic theorem provers)
           | used in 'hammers, like E, Spass, Vampire, have the opposite
           | strengths and weaknesses: they are good at handling
           | quantification, but not so good at theory solving. Moreover,
           | all widely used ATPs tend to be for first-order classical
           | logic, while Lean is based on higher-orders constructive
           | logic. So there is still a gap to be bridged.
           | 
           | It is great to see that people work on this problem.
        
       ___________________________________________________________________
       (page generated 2024-11-22 23:02 UTC)