[c0balt]

The 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

[nextaccountic]

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