On Tuesday 6 October, OpenAI published mathematical results produced by an internal model and opened a repository for their examination. When checked on 9 October, its catalogue listed 719 manuscripts grouped into 372 families; about 42 per cent of the headline results had a Lean formalisation. OpenAI presents them at different stages of verification and says it will add formalisations as it obtains them. The figure describes a changing collection, not a uniform set of results already certified.
Lean is a language for expressing definitions, theorems and proofs so that a programme can check whether a proof follows from the rules and results included in a project. The checker does not read an explanation as a person would. It checks a formal derivation. When it accepts a proof, we have something important: a coded inferential route that satisfies a precise formulation, under the definitions, prior results and axioms imported into the project.
Formalising a proof can expose gaps, fix exactly what has been proved and allow others to check it again. The certificate has a precise object: a proposition expressed in the formal system, together with the definitions, prior results and axioms it imports. Lean’s documentation explains that the checker verifies whether the proof follows from those elements; establishing that the formal statement corresponds to the mathematical problem in the manuscript requires further examination of the definitions and libraries used.
The checker’s precision does not, by itself, identify anyone who understands the strategy, can explain why it works or knows what changes when a hypothesis is altered. Checking a formal derivation and understanding what it proves are distinct achievements. Lean can settle the first question precisely; the second depends on someone being able to account for the argument and its scope.
Four functions now separated
In mathematical practice, several functions often travel together. Someone proposes an argument, writes it down, answers questions about its steps and defends what follows from it. Publication leaves an object others can examine; authorship also identifies people whom the community can question. Authors do not always master every detail of a long proof, and mathematics knows collective arguments, computer-assisted verification and results that are understood only gradually. What matters is that these tasks can be distributed without disappearing.
Artificial intelligence separates these functions sharply. A model may produce an argument; a formalisation may certify a derivation; a mathematician may make the proof their own by understanding its structure and being able to explain it; a person or institution may answer for its publication. These are four distinct tasks: producing, certifying, understanding and assigning responsibility. Here, assigning responsibility means identifying who must correct the record and take editorial responsibility. That attribution does not show that anyone can reconstruct the argument or assess a substantive mathematical objection.
OpenAI’s repository makes the separation visible. The company says the collection contains results at different stages of verification, that not all have Lean formalisations and that some unformalised results could have issues. It also preserves revisions and versions. Alongside the catalogue, it published ten abridged summaries of the model’s reasoning: explanations of selected results, not exhaustive transcripts of the process behind every manuscript. “Published”, “formalised” and “verified by experts” describe different states; keeping them distinct shows what the available materials establish and what remains to be examined.
The validity of a proof and an understanding of its method answer different questions. A machine may have found a correct proof whose idea is not yet transparent to mathematicians; its correctness still stands. What is limited is something else: how much we can claim about the explanation, the method’s fertility and the possibility of reusing it.
The difference between getting it right and teaching it
A proof can contribute more than establishing its conclusion. It can reveal why a conjecture was true, what structure it concealed and which neighbouring problems have now become accessible. If a community checks the result without being able to reconstruct the route, it knows that the conclusion holds and may still not know which general principle is worth learning. The discovery adds a point to the map; understanding can turn it into a road.
This distinction does not require reading the model’s mind. It can be examined publicly by asking whether a system—or the responsible team—can explain the role of each hypothesis, locate the step that fails when a lemma is removed, adapt the proof to a weaker condition and distinguish which conclusion survives. The test is whether it can respond to relevant variations while maintaining continuity between challenge, explanation and revision.
OpenAI published ten abridged summaries of the model’s reasoning, covering selected results. They may orient readers, and their scope matters: they are not exhaustive transcripts of every process. To establish what they show about understanding an argument, each explanation would need to face variations: change a hypothesis, remove a lemma and ask which conclusion survives. The answer would need to follow the proof’s structure. The same test applies to people: human authorship does not certify that an author understands everything they sign.
Institutional responsibility covers another part of the matter. OpenAI can answer for the collection’s selection, editing, attribution and correction procedures. That duty has consequences: preserving versions, documenting changes, providing examinable materials and correcting errors. Editorial responsibility identifies who must take charge of the publication; understanding identifies who can set out a proof’s mathematical reasons. An institution can exercise the first without showing that a particular agent commands the method.
What publication should mean
Publishing AI mathematics would improve if each result stated its status precisely: manuscript available, mathematical review completed, Lean formalisation included, scope of that formalisation and questions still open. An overall percentage describes the collection; it cannot replace an entry for each theorem. For a particular formalisation, readers need to know which statement it checks, which definitions and imports it uses, and whether it covers the central result or only one component.
That entry should also include the revision history and an explanation that allows others to test the argument under controlled changes. If a team can show why a hypothesis is necessary, which part of the reasoning adapts to a neighbouring case and where it stops working, the result gains something the certificate never promised: transferable understanding. If the team cannot yet do that, the honest description is narrower and no less interesting: a formally checked derivation, with its mathematical scope and interpretation still under examination.
OpenAI says it wants its results to advance the frontier of knowledge and will fund gatherings devoted to understanding them. For that purpose to be met, those gatherings must help establish what has been proved, how the formal statement corresponds to the mathematical problem and what independent mathematicians can confirm. Making results accessible means more than uploading files: it requires explaining the scope of each formalisation and allowing others to examine, correct and extend the work.
A certificate can preserve a proof intact and let anyone check it again; by itself, it does not identify someone able to answer for its reasons. That capacity is shown by explaining, accepting variations, correcting and stating what can be learned from the result. In automated mathematics, the checker can already close a proof. The remaining task is to make clear what it proves and who can explain it.