Definition
Formal Theorem Proving is the practice of constructing mathematical proofs in a machine-readable language such that a proof assistant or compiler can mechanically verify every logical step is valid. Unlike informal proofs reviewed by human mathematicians, this approach provides a hard correctness guarantee — a proof that compiles in a system like Lean is, by construction, free of gaps or logical errors that a reviewer might overlook.
Episodes covering this
Worth reading next
Papers we haven't done a deep dive on yet, but would recommend on this topic.
- Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
- Hypertree Proof Search for Neural Theorem Proving
- Verified Multi-Step Synthesis using Large Language Models and Monte Carlo Tree Search
- Autoformalization with Large Language Models
- LEGO-Prover: Neural Theorem Proving with Growing Libraries
- LeanDojo: Theorem Proving with Retrieval-Augmented Language Models