Three years of experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers

282 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models (2024, methodology): “Following Jiang et al. (2022), we leverage models to generate proof sketches, and execute the off-the-shelf automated prover Sledgehammer (Paulson, 2010) to fill in the missing details.”
Autoformalization with Large Language Models (2022, methodology): “In evaluation, whenever the special token is emitted, Thor invokes the proof method Sledgehammer [36] in Isabelle with a 30 second timeout.”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, methodology): “Hammers are available in many ITPs [Paulson, 2010, Kaliszyk and Urban, 2015, Gauthier and Kaliszyk, 2015, Czajka and Kaliszyk, 2018] and are immensely popular within the theorem proving community.”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “In this work, we choose to experiment with Isabelle for three reasons: (1) Isabelle’s proof corpus is one of the largest among interactive theorem provers, conducive to the language models’ mastery of its syntax; (2) Isabelle supports the declarative proof style (detailed discussion in Appendix A), ”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, unknown): “For example, Sledgehammer (Paulson & Blanchette, 2010) translates theorems in the Isabelle proof assistant (Paulson, 1994) to ﬁrst-order logic.”