Proof Assistant

A proof assistant is a computer program with which mathematical proofs are written down and checked. The human specifies each step, and the program verifies whether it truly follows from what came before. If a justification is missing, the software reports this immediately and does not accept the proof. For this to be possible, everything must be written in a very strict language in which every word is precisely defined. Colloquial phrasings such as "it is obvious that" are not permitted there. Well-known programs of this kind are called Lean, Coq (today Rocq), and Isabelle.

Why mathematicians leave the checking to a machine

Modern mathematical proofs are often hundreds of pages long. No human can hold them completely in their head. Reviewers at academic journals sometimes need years to check them, and errors still slip through. A famous example is the classification of finite simple groups: the proof spans tens of thousands of pages by hundreds of authors, and gaps were only noticed decades later.

A proof assistant shifts where trust is placed. One no longer has to hope that all reviewers were attentive. One only has to trust the very small core of the program that implements the logical rules. This core is deliberately kept so small that experts can fully verify it.

The second reason is software safety. Programs in aircraft, chips, or encryption must not contain errors. Testing only ever finds the errors someone thought to look for. A formal proof, by contrast, shows that a program works correctly under all possible inputs. The seL4 operating system kernel and parts of Intel's and AMD's chips have been secured in this way.

From claim to verified proof script

First, the statement is translated into the formal language of the system. "Every even number greater than two is not a prime number" becomes a line of symbols whose meaning is unambiguously fixed. This translation is often the most laborious part of the work. One must also define all the terms used, down to the basic axioms.

After that, the proof is written as a sequence of instructions called tactics. A tactic might say, for instance: "perform a case distinction" or "apply this known theorem." The system continuously shows what still remains to be shown. So one works as if on a task list, working through it step by step until nothing is left open.

It is important to distinguish this from fully automatic provers. A proof assistant does not come up with the proof idea itself; it only checks. It merely takes simple routine steps off one's hands. One can think of it as an extremely pedantic proofreader: it has no ideas of its own, but it also never overlooks a single gap.

Lean, AI systems, and mathematics competitions

In the news, proof assistants usually appear alongside artificial intelligence. Language models occasionally invent false justifications that sound convincing. A proof assistant can expose this because it checks every step. That is why research labs couple their models to systems like Lean: the AI proposes proof steps, and the program filters out the incorrect ones.

This is also how the results at the International Mathematical Olympiad worked. Systems such as AlphaProof from Google DeepMind generated proofs in Lean, which were then checked mechanically. The advantage of this coupling: training receives a reliable signal about whether a solution is correct. With ordinary text, this cannot be decided so unambiguously.

Outside of research, you will mainly encounter this topic in safety-critical technology. When a manufacturer advertises "formally verified" software or hardware, there is almost always a proof assistant behind it. In mathematics, there are also large community projects such as Mathlib, an open library with over a million formally verified lines of proof.