Sledgehammer
Fewer than 5 people recommend it so far, so there's no written verdict. Here is what commenters said.
2recommend
0warn against
Nov 6, 2025first mention
Apr 27, 2026latest mention
Why people recommend it
“It's not perfect but it's remarkably useful”
“Plumbing them together is a serious research contribution”
Caveats and dissent
No one in these comments warned against it.
Often compared with
Threads where it came up
- "Why not just use Lean?" 2 mentions
- First Proof 1 mention
- AI solves Erdos problem #728 (Terence Tao mathstodon post) 1 mention
- Mathematical exploration and discovery at scale 1 mention
Quotes are verbatim; the verdict and theme labels are written by a model from these comments, and every clause links to its sources.
All comments 5
“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.”
“makes sledgehammer sound identical to Mathlib's `grind`”
“sledgehammer is used to crack a lot of nuts”
“It's not perfect but it's remarkably useful”
“Plumbing them together is a serious research contribution”