OpenAI Posts 722 Math Papers From an Unreleased Model on GitHub

A few days ago, OpenAI posted 722 math papers on GitHub. An internal frontier model that has not yet been released generated them. The topics are number theory, algebraic geometry, analysis and combinatorics. Some of the results come with formal proofs in Lean. The Chinese outlet Jiqizhixin states the implications bluntly: AI has begun producing new mathematics faster than mathematicians can understand it, and the community will need years to digest it all.

What exactly was published

The sheer scale stands out. More than seven hundred papers in a single batch, spanning several areas of mathematics at once. Output like that normally accumulates over years and across dozens of authors.

The available portion of the material cuts off at the repository description. As a result, several important details are unknown: how the files are organized, what license the texts are released under, how many people took part in selecting them, and whether the papers went through peer review. OpenAI has not released the model itself, so outsiders cannot reproduce the result.

• 722 papers in an open repository on GitHub
• Source: an internal, unreleased OpenAI model
• Areas: number theory, algebraic geometry, analysis, combinatorics
• Some of the papers have formal verification in Lean
• Status of independent review: not stated in the available material

The bottleneck has shifted to verification

Lean acts as a safety net here. It is a proof system in which a compiler checks every step. If a proof compiles, it has no logical gaps. But some questions remain that the machine cannot settle. Does the formalized statement match the one claimed in the paper? Is the result interesting, or is it a side consequence of something already known? Does it fit into an active line of research?

For papers without formalization, the picture is worse. A human has to read them, and reviewing a single complex paper takes weeks, sometimes months. 722 texts turn that queue into a problem that hiring a couple of extra reviewers cannot solve.

The second half of the Jiqizhixin headline says that mathematicians have "lost their research projects." The mechanism is simple. If a model closes a problem that a graduate student planned to spend a year and a half on, the topic loses its value before the student can defend. This is the outlet's assessment, not a confirmed fact about any specific people, but the logic is clear. Those who work on technical, easily formalized problems are at the greatest risk.

How to deal with it

Mathematicians should check their current topics against the repository. It is better to find overlaps now than after submitting a preprint. It also makes sense to learn Lean, at least well enough to read it: the ability to quickly check someone else's formalization is becoming a working skill.

Journals and arXiv-like platforms will have to settle on a policy. Do they accept texts written by a model, and do they require a formal proof as a condition of review? Without one, the flow of machine-written papers will simply clog the queue.

Engineers and team leads can take away a broader lesson. Formal verification is moving out of its academic niche and becoming a way to accept AI output without taking it on trust. The same principle applies to code and critical systems.

Finally, until independent analyses appear, it makes sense to hold off on sweeping conclusions. The key metric for the coming months is what share of the 722 papers survives checking, and how many of them turn out to be substantive rather than merely correct.