alt Hacker NewsThe goal (ATP) is similar but the idea is a bit different, sledgehammer is not directly learning/applying rules but instead effectively a driver for invoking a bunch of ATPs + SMT solvers at once on a goal in Isabelle/HOL.
You can read more about it here: https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf
The authors of Lean also wrote a smt solver (Z3). Other proof languages like F* use Z3 to prove its things
Why isn't there a tactic in Lean to prove things by SMT using Z3? This could be integrated to grind