Formalization of Proofs

Mathematical proofs are normally written in ordinary language — with formulas, but also with sentences like “it obviously follows that.” A human understands such gaps, a machine does not. In the formalization of proofs, a proof is therefore translated into a strict, machine-readable language in which every single step is explicitly justified. A program called a proof assistant then automatically checks each step. If even a single step cannot be derived without gaps, the assistant does not accept the proof. The result is a level of certainty that goes beyond what human reviewers can achieve — even for proofs that run hundreds of pages long.

Why formal proofs are changing mathematics

In mathematics, a proof is considered correct when experts have read it and found it convincing. This system has worked for centuries, but it has a weakness: humans make mistakes and overlook gaps. The proof of the Four Color Theorem from 1976 was so long and computer-assisted that mathematicians argued for years over whether it was even valid. A formalized proof would make such disputes impossible from the outset.

The consequences reach far beyond mathematics. Safety-critical software — such as in aircraft control systems or medical devices — can be checked using the same methods. Anyone proving that a program works correctly under all circumstances needs the same apparatus as someone formalizing a mathematical theorem.

What happens inside a proof assistant

Proof assistants like Lean, Coq, or Isabelle are specialized programming languages. In them, one writes not only what one is claiming, but also how each step is justified. The system knows basic axioms — that is, rules assumed to be true — and checks whether every inference can be derived from these axioms. If something is wrong, an error message appears, just as with a typo in an ordinary computer program.

This process is laborious. A proof that takes up two pages on paper can require thousands of lines once formalized. Many steps that a human skips as “obvious” must be explained to the computer individually. This is precisely where AI models have recently entered the picture: they are meant to automatically fill these gaps and relieve humans of the typing work, without sacrificing the rigor of the process.

An important difference from ordinary computer programs: the proof assistant cannot deliver “almost correct.” Either the proof is completely correct, or it is not. There is no gray area.

Formal proofs in current AI projects

Formalization of proofs appears in tech news primarily in connection with mathematical AI systems. Google DeepMind and OpenAI are working on models intended to solve mathematical problems independently — at a level required by international olympiad competitions such as the IMO. The decisive test here is not whether the model provides a plausible-sounding answer, but whether its solution path is accepted by a proof assistant.

The Lean ecosystem has built up a large collection of formalized mathematics in recent years, the so-called Mathlib. This library contains thousands of verified theorems on which new proofs can build. AI models are now being trained to work with it. Formalization thus becomes the benchmark for whether an AI model is truly reasoning mathematically — or just sounding convincing.

A common misconception is to confuse formalization with merely solving calculation problems. A calculator computes, but it proves nothing. A proof assistant, by contrast, shows that a result holds under all conceivable conditions — a fundamentally different and stronger claim.