Imagine a proofreader who understands nothing of what they read, but checks that each sentence follows properly from the previous ones according to rules written in advance. They cannot judge whether the reasoning is interesting, nor whether it answers the right question. They can guarantee there is no gap. That is exactly what a proof assistant is, and it is far more useful than it seems.
We reported this morning on a mathematical proof obtained with models and formally verified. Here is how it works.
The principle
A proof written in natural language always contains shortcuts: "it is easy to see that", "the next case is analogous", "by a standard argument". These shortcuts are useful among specialists, and that is where most errors hide.
Formal verification removes these shortcuts. The proof is rewritten in a language where every step must be justified explicitly, relying on logical rules and on previously established results.
A program then scans the whole thing and mechanically checks that every deduction is valid. If it accepts, the proof is correct in the strict sense. If it refuses, it indicates where things get stuck.
Why trust the verifier
The natural question is: why believe this program rather than the proof?
The answer lies in an architectural property. These systems are built around a minimal kernel: a few hundred lines of code implementing the basic logical rules. Everything else in the system, which is huge, must go through this kernel to validate anything.
So to trust the whole, you only need to trust this small kernel. It is relatively simple, it has been audited by many people, and it has not changed for years.
This is the shift we described in our article on trust: you do not understand the object, you understand the device that checked it.
The statement is not verified. The system guarantees that the proof demonstrates what is written. If the formalised statement does not match the question you meant to ask, the proof is perfectly valid and beside the point. This is the most common error, and it requires a human re-reading of the statement alone — which is short.
Interest is not judged. A verifier accepts a trivial proof as readily as a major result.
The cost remains high. Formalising a proof takes far longer than writing it. This is what long limited the practice, and it is precisely what models are changing.
Why it is becoming central now
Two movements are converging.
Models produce volume. They can propose dozens of avenues, attempt constructions, produce proofs. The bottleneck shifts from production to verification.
Models make formalisation less costly. Translating a proof into a formal language is tedious, repetitive work where errors show up immediately since the verifier refuses. This is exactly the kind of task profile we described as automatable in our article on what deserves to be automated.
The combination is virtuous: the model proposes and formalises, the verifier guarantees. The model's main flaw — producing the plausible with confidence — is neutralised by a device that cannot be persuaded.
Beyond mathematics
This approach already applies elsewhere, and that is little known.
Critical components of transport, aeronautics or cryptography software are formally verified: the program is proven to do exactly what its specification describes, rather than being tested on cases.
This is an interesting avenue for code produced by models. We noted regarding modernised scientific code that the danger comes from programs that run perfectly while producing a wrong result. A verification device would remove that class of errors — for the properties one thought to specify.
What to remember
Formal verification is not an AI technology, and it is becoming its most useful complement.
It offers a concrete answer to the question we keep asking: how to use a system that is often right and sometimes wrong, without being able to tell the two apart? The answer is not to trust better, it is not to have to trust at all.
This principle extends well beyond mathematics. Wherever one can mechanically define what a correct result is, one can let a model produce a lot and have a verifier sort it out. Where one cannot define it — judgement, taste, relevance — we will have to keep reading.