autoformalization
In plain wordsUsing AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify.
The automatic translation of informal mathematical text, natural language mixed with notation, into a formal language 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., Isabelle/HOL or 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., producing statements and proofs that a proof assistant can check. Statement autoformalization supplies training data for AI provers — 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. was trained on about 80 million formal statements produced by autoformalizing informal problems (Nature, 2025) — and formal statements let 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. use proof checking as a reward. Proof autoformalization turns human or model-written arguments into machine-checked ones. The central difficulty is faithfulness: a formal statement can type-check yet mean something other than the original, so outputs are validated by back-translation, agreement across samples or human review. The technique is also applied to software specifications, regulations and scientific claims.
Autoformalization turned 9,000 textbook exercises into Lean statements, of which reviewers judged about 70 percent faithful.
Origin
Pursued from the mid-2010s by Cezary Kaliszyk, Josef Urban and colleagues, who trained statistical and later neural translators on aligned informal and formal corpora, and advocated by Christian Szegedy in 2020 as a path toward general AI. Yuhuai Wu and colleagues' 2022 paper showed that large language models could correctly formalize a substantial fraction of competition problems.
Usage note
Misformalization — a correct proof of the wrong statement — is the characteristic failure. Autoformalization is the translation step; once a statement is formal, checking a proof of it is mechanical.
Related
- 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.
- 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.
- 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.
- 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.
- semantic parsingsemantic parsing, n.: Translating a sentence into a precise, machine-executable form — such as a database query or a logical formula — so that a computer can act on what was asked.
- 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.
Sources
- Szegedy, C. (2020). A Promising Path Towards Autoformalization and General Artificial Intelligence. Intelligent Computer Mathematics (CICM 2020), LNCS 12236.
- Wu, Y., Jiang, A. Q., Li, W., Rabe, M. N., Staats, C., Jamnik, M. & Szegedy, C. (2022). Autoformalization with Large Language Models. NeurIPS 2022.
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., 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., 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., 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., 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.