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 34 days ago [-]
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.
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.