Comment by thaumasiotes
21 hours ago
> Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean.
I have no knowledge of what sledgehammer is. However...
> it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer"
This description makes sledgehammer sound identical to Mathlib's `grind`. https://leanprover-community.github.io/mathlib4_docs/Init/Gr...
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
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