2 ms·

> 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. Ho

> 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/Grind/Tactics.html https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

c0balt 6mo ago
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 https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf
- nextaccountic 6mo ago
  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