AI in Mathematics: Why Formal Verification Is the Interesting Part

Nearly every discipline in this cluster has an expensive verification step, and that is what limits how much a model can help. Mathematics is the exception: a formal proof can be checked mechanically, in seconds, with certainty. That single property changes what a language model is allowed to be used for.

What makes mathematics unusual

An ordinary mathematical paper is a proof written for a human reader. It compresses, it says “similarly”, it leaves routine verifications to the reader. Correctness is established socially, by referees and by other mathematicians using the result. That process works well and it occasionally fails — errors have survived in the literature for years.

A formal proof is a different object. Every inference is written in a fixed logical language and every step is checked against the axioms by a small program called the kernel. Proof assistants such as Lean, Coq and Isabelle are built around this, together with large shared libraries of already-formalised mathematics, so a new proof can appeal to results that have themselves been checked. Substantial theorems have been formalised this way, including the four colour theorem, the odd order theorem and Kepler’s conjecture on sphere packing — the last of which was formalised precisely because the original proof leaned on computation that referees could not fully check by hand.

The kernel changes the failure mode

Ask a language model for a proof in prose and you get the failure that next-token prediction makes structural: a fluent, confident, plausible-looking argument with a false step buried in it. Mathematics is the worst possible domain for that, because a proof with one bad step is worth nothing and spotting the bad step is the hard part.

Put the same model inside a proof assistant and the character of the failure changes entirely. A proposed step is either accepted by the kernel or rejected. There is no such thing as a convincing wrong step, because convincingness is not what is being evaluated. The model can be wrong as often as you like; it cannot be wrong in a way that survives.

This is the general pattern worth taking from the page, and it applies well beyond mathematics: the trustworthiness of a model-in-a-loop comes from the checker, not the model. Where you can build a cheap, sound, automatic checker — a type system, a test suite, a simulator, a diffraction refinement, a proof kernel — a mediocre generator becomes useful, because you can afford to throw away almost everything it produces. Where you cannot, a much better generator helps much less.

The model as a proposer in a loop

What that looks like concretely, inside a proof assistant:

• Premise selection. Mathematical libraries contain enormous numbers of lemmas. Deciding which handful might apply to the current goal is a retrieval problem, and it is one neural methods are straightforwardly good at.
• Tactic prediction. Proof assistants are driven by tactics — commands that transform the goal. A model trained on existing formal proofs suggests the next tactic, the assistant applies it, and the resulting proof state is the feedback.
• Search. Proof states form a tree. Tactic suggestions are the branching, the kernel is the environment, and closing the goal is the terminal reward. Because the reward is machine-checkable rather than learned, reinforcement learning here does not have the reward-model problem that makes it awkward for open-ended text.

Systems built on this pattern have produced formally verified solutions to competition problems at a level that would have seemed implausible a few years earlier, including at olympiad standard, sometimes by pairing a neural proposer with a symbolic deduction engine that handles the parts classical methods are already good at. The verified part is the load-bearing claim: those solutions were not judged by a human to look right.

The other two uses: search and conjecture

Formal proof is not the only place a checker exists. In combinatorics and related areas, a construction can often be represented as a program whose quality is computed by running it — the size of a set, the ratio achieved by a heuristic. That makes an evolutionary loop possible: a language model proposes programs, an evaluator scores them, the best are fed back into the prompt, and the loop runs for a long time. This has produced improved constructions on open problems where the previous best was a human-designed object, and the improvement is verifiable by anyone who runs the program.

The third use is different and is closer to how mathematicians actually work. Train a model to predict one mathematical invariant from others on a large collection of examples; if it succeeds, there is a relationship to find. Then use attribution techniques to see which inputs the prediction depended on, and hand that to a mathematician, who looks for the theorem. Published work has done exactly this, with the human proving the resulting statement. The model contributed the direction, not the proof — which is a real contribution and a modest one, and reporting it that way is what made it credible.

Why competition results do not extrapolate

• Formalisation is the bottleneck, and it is human work. Translating an ordinary research paper into a proof assistant is a substantial project. Until autoformalisation is reliable, most mathematics simply is not in a form a checker can touch, so the loop above is unavailable for it.
• Competition problems are a curated distribution. They are short, self-contained, have a known solution, and are guaranteed solvable within a few hours by a talented teenager. Research problems have none of those properties, and the last one is doing more work than it appears: a search that terminates is a different task from a search that might never terminate.
• Contamination is a live concern. Competition problems and their solutions are on the public internet, which is where the training data came from. This is the standard difficulty described in benchmark contamination, and it is why blind, freshly-set problems carry so much more weight than a score on an archive.
• A verified proof is not necessarily an understood one. Mathematicians want proofs that explain. A long machine-found certificate that no one can read establishes the theorem and does not deliver the thing the theorem was wanted for.