From AI Ideas to Checkable Mathematics

Picture opening a research repository expecting one polished paper and finding an entire shelf: manuscripts, source files, proof code, build instructions, and revision history. That is the striking part of OpenAI’s October 6, 2026 release on AI progress in mathematics. The announcement is not only a claim that an internal model found new results. It is also an attempt to show how those results can be handed to a community that must inspect, cite, correct, and explain them. (openai.com)

The repository currently describes 722 manuscripts grouped into 372 families. They sit at different stages of verification: many have Lean material, but not all do, and the project warns that unformalized results may contain problems. (github.com)

“AI proved it” hides three different jobs

A conjecture is a mathematical claim that still needs proof. A proof is a chain of deductions showing that a claim follows from definitions, earlier results, and accepted rules. An AI system may help with the first job by suggesting a surprising pattern or a possible route through a difficult problem, but discovery is not the same as verification.

There is also a third job: exposition. A result has to be written clearly enough for another mathematician to understand what was claimed, why it matters, and where each step comes from. That gives us three separate checkpoints: the model may generate an idea, a human-readable manuscript may explain it, and a formal system may check a machine-readable version of the argument. A release becomes much more useful when it exposes all three rather than presenting a polished conclusion alone.

Lean turns a proof into an artifact

Lean is a programming language and theorem prover used to express mathematics in a form that software can check. A proof assistant is a tool that helps write formal proofs and verifies that every step follows inside a specified logical system. Instead of asking whether an argument “looks right,” you give Lean precise definitions, propositions, and proof commands. Its small trusted core then checks the resulting proof object. (lean-lang.org)

A tiny example looks like this:

import Mathlib

example: (2: ℕ) + 2 = 4:= by
 norm_num

Here, ℕ means the natural numbers, and norm_num is a tactic that normalizes numerical expressions and closes elementary arithmetic goals. This example is not deep mathematics. Its value is that it shows the basic bargain: the statement is precise, the proof is executable, and Lean either accepts it or reports a failure. (leanprover-community.github.io)

A serious Lean formalization—the process of translating a mathematical argument into this machine-checkable language—can be far longer. It may require definitions for the objects in the theorem, small lemmas that a paper leaves implicit, and a carefully specified library environment. That extra work can feel tedious, especially when the informal proof seems obvious. It is also where hidden gaps often become visible.

Checkable does not mean finished

This is the part that deserves patience. A formal checker can establish that an encoded proof follows from its encoded assumptions. It cannot decide whether the encoding captured the author’s intended theorem, whether the result is genuinely novel, or whether the exposition gives humans a useful understanding of the idea.

The OpenAI repository makes that distinction explicit by labeling results according to their verification stage and noting that not every manuscript has a Lean formalization. A proof that has not yet been formalized may still be valuable, but it should be treated as research material rather than a finished, independently verified theorem. (github.com)

Formal proofs also live inside a foundation of imported definitions, lemmas, and assumptions. Readers therefore need to inspect more than a green build: they need to understand what was formalized, which parts remain conditional, and whether the machine-checked statement matches the mathematical claim in the paper. Lean can be a powerful second pair of eyes, but it does not replace mathematical judgment.

Transparency is part of the result

The release publishes more than manuscripts. It includes revision and citation protocols, ten abridged reasoning summaries, estimates of compute, and statistics about attempted problems. The repository reports approximately 4,000 problems posed during the evaluation, with the average result using compute equivalent to about three hours of ChatGPT Pro thinking. (openai.com)

Those numbers do not prove that the results are correct. They provide provenance: a record of where the collection came from and how much searching stood behind it. That matters because the final catalogue is not the output of one lucky prompt. It is the result of generating many attempts, selecting some as significant, grouping related work, and continuing to formalize and revise the survivors.

Version history matters for the same reason. If a manuscript changes later, readers should be able to see the earlier version rather than having the record silently rewritten. In mathematics, citations are not decoration; they are part of the chain that lets one researcher build on another researcher’s work.

Human review gives the result meaning

The independent Advisory Group on Mathematics and Artificial Intelligence has emphasized that a public release is the beginning of human understanding, not the completion of it. The group also makes clear that its advice is not an endorsement of any individual result or process. (agmai.org)

That framing is useful. Mathematics becomes shared knowledge when other people can inspect a claim, reproduce its argument, challenge its assumptions, explain its importance, and extend it. A model can accelerate the search, but the community still decides what survives as mathematics worth remembering.

The practical workflow looks less dramatic than the phrase “AI proved a theorem”: a model proposes, a mathematician clarifies, a formalizer encodes, Lean checks, and other mathematicians review. Each stage catches different failures. The lasting value of this release will not be measured only by the number of manuscripts it contains, but by how many ideas become understandable, independently checked, and useful starting points for future work.