interactive theorem proving
In plain wordsWriting a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong.
A method of formal proof in which a person steers and a program verifies: the program, a proof assistant, encodes definitions, theorems and proofs in a formal logic, usually higher-order logic or dependent type theory, and mechanically checks every inference. The user states goals and applies tactics — commands that split goals into subgoals or invoke automation — while a small trusted kernel certifies the final proof, so confidence rests on the kernel rather than on the tactics or the user. Major systems include Isabelle/HOL, RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step. (formerly Coq), LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs., HOL Light, Mizar and Agda. Landmarks include machine-checked proofs of the four color theorem (2005), the Feit–Thompson odd order theorem (2012) and the Kepler conjecture (2014), and verified software such as the CompCert C compiler and the seL4 microkernel. Formal proofs supply the unambiguous signal used to train AI provers.
After three months of interactive theorem proving, every lemma in the paper had been checked by the kernel.
Origin
Nicolaas de Bruijn's Automath (1967) and Andrzej Trybulec's Mizar (1973) pioneered computer-checked mathematics. Robin Milner's LCF (Stanford 1972, Edinburgh 1979) introduced the small trusted kernel and the ML language for writing tactics, the template for HOL, Isabelle and many later systems.
Usage note
Interactive and automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement. increasingly merge: proof assistants call automated provers ('hammers'), and language-model provers generate proofs that the assistant checks. Autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify. tries to automate the translation from informal mathematics. A proof certifies only its formal statement, so mistranslated definitions remain a risk.
Related
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
- RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step.
- autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify.
- formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way.
- first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
Sources
- Gonthier, G. (2008). Formal Proof — The Four-Color Theorem. Notices of the AMS 55(11), 1382–1393.
- Hales, T. et al. (2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi 5, e2.
Mentioned in
automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement., deductive reasoningdeductive reasoning, n.: Reasoning in which true starting points guarantee a true conclusion: if every square is a rectangle and this shape is a square, then it must be a rectangle., first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI., formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way., LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs., verifierverifier, n.: A program or AI model that checks whether a proposed answer is correct — by running tests, comparing with a known result or judging the reasoning — so that good answers can be picked or rewarded., autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify., IMO Grand ChallengeIMO Grand Challenge, prop. n.: The goal of building an AI that earns a gold medal at the International Mathematical Olympiad, the top contest for school-age mathematicians. AI systems first reached gold-medal scores in 2025, though not under the challenge's strict original rules., IsabelleIsabelle, prop. n.: A widely used proof-checking program in which people write mathematics and verified software; it is known for automation that calls other theorem provers to finish routine steps., MathlibMathlib, prop. n.: A huge shared library of mathematics written in the Lean language, in which every definition and proof has been checked by computer. Mathematicians keep extending it, and AI proof systems are trained on it., RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step.