automated theorem proving
In plain wordsGetting 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.
The use of programs to find proofs of conjectures from axioms in a formal logic without step-by-step human guidance. Classical provers work in 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., usually with equality, and search for refutations using resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known. and superposition calculi, tableaux or instantiation-based methods, as in Vampire, E and Prover9; decision procedures and SMT solverssatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met. handle specific theories such as arithmetic. They excel at large numbers of shallow proofs, as in hardware and software verification, but struggle with deep mathematics, where human-guided interactive theorem provinginteractive theorem proving, n.: Writing 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. dominates. Since about 2020, neural provers pair language modelslarge language model, n.: A computer program trained on enormous amounts of text to predict the words that come next. At vast scale, that simple skill lets it chat, answer questions, translate, summarize and write code. that propose proof steps or whole proofs with a proof assistant such as 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. that checks them, and are trained by reinforcement learningreinforcement learning with verifiable rewards, n.: Training an AI by letting it attempt problems whose answers can be checked automatically — a math result, a passing program — and rewarding it only when the check succeeds. on the checker's verdicts — the approach of AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time. and DeepSeek-Prover.
The automated prover discharged 70 percent of the verification conditions; the rest went to the proof engineers.
Origin
Martin Davis's 1954 implementation of Presburger's decision procedure for the arithmetic of addition and Newell, Shaw and Simon's Logic TheoristLogic Theorist, prop. n.: A 1956 computer program that proved theorems from a classic logic textbook by searching cleverly rather than trying every possibility. Many historians count it as the first AI program. (1956) were the first theorem-proving programs. Hao Wang's 1958–1959 programs proved hundreds of theorems of Principia Mathematica, and J. Alan Robinson's resolution principle (1965) set the field's course. In 1996 William McCune's EQP proved the Robbins conjecture, open since the 1930s.
Usage note
Usage varies: some reserve 'automated' for fully automatic provers and treat proof assistants separately, while 'AI theorem proving' now often means language-model provers that emit formal proofs for a checker. A machine-checked proof is only as trustworthy as its formal statement.
Related
- interactive theorem provinginteractive theorem proving, n.: Writing 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.
- resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known.
- 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.
- satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.
- 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.
- AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time.
- 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.
- interactive theorem provinginteractive theorem proving, n.: Writing 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.
Sources
- Robinson, J. A. (1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12(1), 23–41.
- McCune, W. (1997). Solution of the Robbins Problem. Journal of Automated Reasoning 19(3), 263–276.
Mentioned in
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., FrontierMathFrontierMath, prop. n.: Several hundred new math problems, kept unpublished so AI systems cannot have trained on them, written by professional mathematicians to check whether machines can do advanced, even research-level, mathematics., interactive theorem provinginteractive theorem proving, n.: Writing 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., International Mathematical OlympiadInternational Mathematical Olympiad, prop. n.: The world's top math competition for high-school students. Because its problems demand creative written proofs, not just answers, earning a gold medal there became a famous test of AI reasoning, first passed in 2025., 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., Logic TheoristLogic Theorist, prop. n.: A 1956 computer program that proved theorems from a classic logic textbook by searching cleverly rather than trying every possibility. Many historians count it as the first AI program., reasoningreasoning, n.: Working out conclusions step by step from facts, rules or evidence, as in solving a math problem or planning a trip. Whether today's AI truly reasons, or imitates reasoning, is debated., AlphaGeometryAlphaGeometry, prop. n.: A Google DeepMind system from 2024 that solves olympiad geometry problems nearly as well as top human competitors, by pairing a language model that suggests constructions with a logic engine that checks every step., AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time., 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., Gödel machineGödel machine, n.: A purely theoretical design, proposed by Jürgen Schmidhuber, for a program allowed to change anything about itself, including how it learns, but only once it has proved that the change is an improvement., 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., miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically., PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics., resolutionresolution, n.: A mechanical step of logical reasoning: from 'A or B' and 'not A or C', conclude 'B or C'. Repeating it can demonstrate any conclusion that genuinely follows from what is known., 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., satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met., unificationunification, n.: Finding values for the blanks in two logical patterns so that they become identical, for example matching 'parent(X, bob)' with 'parent(alice, Y)' by setting X to alice and Y to bob.