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.
Similar to sledgehammer in Isabelle/HOL.
A bit of history: Sledgehammer became fully operational in 2007, extended to call external SMT solvers in 2008. Looks like Lean is catching up.
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.