Autoformalization
Autoformalization refers to the automatic translation of mathematics written in natural language into a strictly formal notation that a computer can check step by step for errors. AI models take over the translation work that previously had to be done laboriously by hand by humans.
Mathematics is normally written down in a mixture of language, formulas, and sketches. A human understands a proof like this, a computer does not. For a program to actually verify a proof, every step must be written in a strictly defined artificial language that has no gaps and no ambiguity. Rewriting into this artificial language is called formalizing, and it is extremely laborious: a single page of textbook text can easily take days. Autoformalization means having an AI perform this translation. A sentence like “every even number greater than two is the sum of two prime numbers” is then automatically turned into an expression that verification software can process.
What makes formal proofs so valuable
With a formally checked proof, there are no more cases of doubt. The software either accepts it or it doesn’t. Human reviewers, on the other hand, sometimes overlook errors, especially in proofs spanning hundreds of pages. There have been several instances in the history of mathematics of results that were considered proven for years and later turned out to have gaps.
The second reason concerns the AI itself. Language models are known to make up things that sound plausible but are false. In mathematics, this often only becomes apparent much later. But if a model delivers its proofs in formal form, the verification software can immediately render a verdict. This gives you a signal that is not based on opinion, but on computation.
This very signal can be used for training. A model can produce thousands of proof attempts, the software filters out the incorrect ones, and training continues with the correct ones. Such cycles are considered one of the most promising ways to make AI better at logical reasoning. The bottleneck here is the amount of formalized tasks—and autoformalization is meant to remove it.
From a line of text to a checkable expression
The formal artificial language comes from so-called proof assistants. Well-known examples are Lean, Isabelle, and Coq. You can think of them as programming languages for mathematics. They know only a few basic rules and derive everything else from those. A proof in them is a program, and the checking is essentially a very strict compiler run.
A language model is now trained on pairs: on the left the text in natural language, on the right the formal version. After enough examples, it can attempt the translation itself. The proposal then goes directly to the proof assistant. If it reports an error, the error message goes back to the model, which makes a new attempt. Often dozens of such rounds run before an expression passes.
One pitfall remains, however. The proof assistant only checks whether a statement is correctly proven—not whether it is the intended statement. If the model translates the task incorrectly, a flawless proof of the wrong claim is produced. Two tasks are therefore distinguished: the formalization of the statement and the subsequent finding of the proof. Only the second one is truly reliably checked by the software.
Competition problems, Mathlib, and chip design
The topic is most visible in mathematics olympiads. Systems like AlphaProof from Google DeepMind automatically formalized competition problems and then solved them in Lean. In 2024, this was enough for a silver medal at the International Mathematical Olympiad. Such reports now appear regularly in tech news.
At the same time, Mathlib is growing, a shared library of formalized mathematics for Lean. It contains well over a million lines of proof, typed by volunteers from all over the world. Autoformalization is meant to multiply this pace. Large projects, such as the formalization of modern research papers, would otherwise be hardly manageable.
Outside of pure mathematics, chip and software companies use the same technique. Processors and safety-critical programs are formally verified so that certain errors can be demonstrably ruled out. There, too, writing down the requirements is the expensive work. Whoever can automate it saves considerable costs—which is why not only research but also industry is interested in this topic.