When an AI proposes a proof, the question is not simply whether its text seems convincing. We need to be able to check the reasoning, understand exactly what has been proved and determine what the result changes. Lean plays a part in this process, with a particular strength: its checks apply to a formalised proof. That does not, however, turn every announcement accompanied by the word ‘verified’ into a discovery that is definitively understood.
On 26 October 2026, OpenAI claimed three results in mathematics, theoretical computer science and physics. The company announces a proof of the local smoothing conjecture in all dimensions, with consequences for Kakeya, a refutation of the exponential time hypothesis, and an existence result in quantum field theory. It describes a differentiated release: public materials for the first two strands, while publication of the physics documents is left to the group of researchers tasked with studying them.
These claims bring a distinction to the fore: producing a proof, verifying it and establishing its significance are three related but different tasks.
What Lean actually receives
The Lean project documentation explains that proof scripts and tactics produce an explicit object called a proof term. A restricted component, the kernel, then checks its logical construction. A tactic is the means used to search for or assemble the proof; it is not, by itself, what makes the proof valid.
This separation matters for AI. A system can suggest a mistaken approach, try an ineffective strategy or generate a very confident explanation: none of these behaviours replaces the object that the verifier has to accept. Checking therefore does not amount to asking a second model whether it finds the answer plausible.
Lean is also a programming language, not just a mathematical proof checker. Its uses include verifying software and protocols. In all these cases, the benefit depends on prior work: expressing precisely the properties we want to establish. A poorly chosen property can be proved perfectly and still be insufficient for the intended use.
The right proof must answer the right question
Consider a deliberately simple example, unrelated to the work announced. Proving that all the even numbers in a collection are divisible by two does not prove that all the numbers in that collection are even. The difference lies in the statement, not the virtuosity of the proof. Yet a hurried reader may draw a broader conclusion than the one actually established.
In research, the gaps are less obvious: the domain of validity, starting conditions, definitions or dependencies can change the scope of a theorem. Human work is therefore not just a matter of admiring the length of a file. The formal statement must be compared with the original question, and checked to ensure that no decisive restriction has crept in between the two.
The Lean manual on validation explicitly distinguishes the validity of a proof from the meaning of its statement. Validation markers in the editor relate to a conclusion obtained from the definitions, theorems and axioms of the project. They are not an independent certificate of the result’s scientific novelty.
Assumptions are part of the result
An axiom is a starting point accepted within the logical framework being used. Adding one is not the same as proving it. That is why the manual recommends inspecting dependencies with the ‘#print axioms’ command. The presence of ‘sorryAx’, for example, indicates reliance on a proof left incomplete in the theorem or its dependencies. Lean’s standard axioms should not be confused with an additional assumption introduced for a particular project.
For more demanding contexts, the documentation also describes rechecking proofs and comparing them with a statement established in a trusted environment. The point is practical: check the right object, with the right assumptions, under the right conditions. The phrase ‘it compiles’ does not, on its own, tell the whole story.
This does not diminish the value of formalisation. On the contrary, making these elements open to examination gives critics something to work with. Scientific discussion can then focus on a precise definition, an identified dependency or a reproducible discrepancy, rather than on the confidence with which a system presents its answer.
AlphaProof: a documented example, not confirmation of OpenAI’s claims
The study ‘Olympiad-level formal mathematical reasoning with reinforcement learning’, published in Nature, describes a different system: AlphaProof. It learns to search for proofs in a formal environment, using attempts and verifiable feedback. A tactic changes the state of the problem; the remaining goals show what still needs to be solved. The result can be checked in Lean.
The authors report solving three of the five non-geometry problems in the 2024 International Mathematical Olympiad. The score equivalent to a silver medal combines AlphaProof and AlphaGeometry 2, with several days of computation. These conditions are part of the performance: they prevent it from being portrayed as the instant result of a general-purpose assistant operating under the same conditions as a human contestant.
This study shows how research and verification can work together. It does not validate OpenAI’s results, which concern different systems and different questions. Moving from success in a competition to a research advance requires evidence specific to each case.
How to read the next announcement
OpenAI presents its manuscripts as raw materials that require work to understand. For the computer science strand, the company announces a group led by Russell Impagliazzo, Ramamohan Paturi and Ryan Williams. The role of such a review is not simply to provide an endorsement: it should make the results open to discussion, explainable and placeable within existing knowledge.
For readers, four questions help keep things in perspective: Is the exact statement accessible? Are the assumptions explicit? Is the verification described in a reproducible way? Do the scientific or practical conclusions go beyond what has actually been established? A positive answer to one does not make the other three unnecessary.
A formal proof can be a considerable result. Its existence does not yet tell us how much a useful computation will cost, which fields will benefit from a method or whether an announced discovery will lead to an application. The strongest promise is more precise: to make part of the reasoning checkable, so that discussion can begin on something other than persuasive text.
Illustrative photograph: a board of scientific formulae, unrelated to the proofs discussed. Vitaly Gariev / Pexels, Pexels licence.
