Discharging Lean goals into SMT solvers

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.