MrKeyoor's tracker counted 1,485 stars on OpenAI's new math repository at 00:20 UTC on October 7, roughly two and a half hours after GitHub says the repo was created. The same repo arrived with its issue tracker and discussions disabled, while pull requests were limited to collaborators. Attention traveled quickly. A route for outside reviewers to report what they find did not open with it.
That mismatch matters because this is no ordinary code dump. OpenAI released 722 AI-generated mathematical manuscripts, grouped into 372 result families, plus Lean proof artifacts for part of the collection. The company's own README says some unformalized results could contain errors. The release therefore gives mathematicians source material to inspect while also handing them a review queue of unusual size.
The 722 count is easy to misread
A manuscript is not the same unit as a mathematical result. OpenAI's repository guide explains that one family can contain a principal result, companion arguments, consequences or alternative proofs. The headline numbers are 722 manuscripts and 372 families. Describing the release as 722 separate breakthroughs would inflate what OpenAI actually published.
The collection came from an unreleased internal model after OpenAI's existing math evaluations had saturated. According to the release announcement, the model was given about 4,000 problems. OpenAI estimates that an average accepted result used the equivalent of roughly three hours of ChatGPT Pro thinking. That is an aggregate compute description, not a recipe an outside researcher can run against the same model.
The catalogue includes claims with enormous mathematical stakes. Its opening entries cover Milne's rationality conjecture and the Birch-Swinnerton-Dyer formula in specified cases, followed by a claimed zero-free half-plane for the Riemann zeta function. Those descriptions come from OpenAI's manuscript map. They should be read as claims attached to manuscripts until specialists check the arguments, their novelty and their relationship to prior work.
OpenAI says it will preserve old versions and record corrections as new ones. It also states plainly that unformalized results may have issues. That sentence sets the right initial status for the collection. Publication makes inspection possible. It does not complete inspection.
Lean covers 162 papers' main results
The repository's machine-readable formalization manifest contains 162 source-paper entries under a comment that describes them as papers with a formalized main result. Compared with 722 manuscripts, that is about 22.4 percent. The counts do not line up perfectly by design, since several manuscripts can belong to one family and a formalization can cover the main theorem without covering every later application in a paper.
The quasi-Riemann-hypothesis family shows why scope needs to be checked line by line. Its Lean documentation says the formalization covers the claimed 7/8 zero-free bound and a uniform gap for real zeros. It also says later applications in the paper are excluded and no explicit value is given for one constant. A label such as "formalized" can therefore be accurate while remaining narrower than the surrounding manuscript.
OpenAI provides a comparator challenge for that family. The repository's checking instructions reduce the first run to four commands after the required tools are installed:
cd lean
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json
Even this path comes with operational details. The Lean directory README recommends compiling small portions because the full library may hit Linux's vm.max_map_count limit. It suggests a build option that disables memory mapping and specific GLIBC_TUNABLES values if that happens. Rechecking a proof is real engineering work, not a green badge attached automatically to every PDF.
Lean's own validation guide draws another boundary. A kernel check establishes that a formal theorem follows from the definitions, theorems and axioms used by the project. It does not establish that the formal statement matches the informal claim a reader thinks it expresses. The guide treats unreviewed AI-generated proofs and programs as potentially malicious for high-assurance checking, which is why comparator builds in a sandbox and can use an external checker. Anyone cloning this collection should use an isolated environment rather than a workstation that holds credentials.
A public repository with closed feedback controls
The repo is public and carries an Apache 2.0 license, so anyone can read it or fork it. At the time of checking, however, the GitHub API metadata reported issues and discussions as disabled. The web interface also stated that only collaborators could create pull requests. Those settings make the repository a distribution channel and version record, with public review pushed into forks, independent notes or channels outside the project.
That choice sits awkwardly beside the release's stated purpose. OpenAI says it consulted the independent Advisory Group on Mathematics and Artificial Intelligence and is exploring community-hosted alternatives. The group's responsible-release recommendations call for papers to live in scholarly repositories outside an AI lab's control, with persistent identifiers, recorded modifications and preferably comments. GitHub supplies a visible history, yet the current project lacks the public conversation tools that would let a specialist attach a counterexample or citation problem to the exact artifact.
A star count cannot fill that role. Stars measure attention and give people a way to bookmark a repository. They say nothing about whether one proof has survived expert review. The early 1,485-star rise tells us developers and researchers wanted to see the files. The slower numbers to watch are corrected manuscripts, added formalizations and independent papers that reproduce or reject individual claims.
Ten reasoning summaries for 372 families
OpenAI published abridged reasoning summaries for 10 selected families, including work on the irrationality exponent of pi and the three-dimensional relativistic Vlasov-Maxwell system. The README table links those summaries, while the broader catalogue contains 372 families. The announcement and repository identify the system only as an internal frontier model.
AGMAI recommended disclosing the model name, prompts, a reasoning summary, time taken and estimated compute for each released result. OpenAI provides the aggregate attempt count, its average compute estimate and 10 reasoning summaries. The public materials do not offer that same provenance package for every family. This limits reproducibility even where a PDF and Lean artifact can be downloaded. An outside group can check the submitted proof, but it cannot rerun the generation process that produced it.
The advisory group also separates machine-checkable correctness from human understanding. Its October 6 statement calls the release the beginning of that process and leaves assessment to the mathematical community. OpenAI says it will fund workshops, conferences and other programs around understanding major AI-produced results. Specific grants, hosts and schedules have not yet been announced. Those details will show whether review receives resources comparable to generation.
What to watch in the repository
The next useful signals are changes that reduce the review burden. Watch whether the 162-entry formalization manifest grows, whether OpenAI enables an issue or discussion channel, and whether the manuscripts move to an independent host with stable identifiers. A correction history tied to individual papers would reveal more than another jump in stars. So would named outside reviews that state exactly which theorem and version they checked.
For now, the repository should be handled like a very large set of candidate patches. Pin the commit before testing, run proof code in isolation, compare each Lean statement with the prose theorem, and record what a successful check leaves unanswered. OpenAI moved 722 manuscripts into public view in one release. Their path into accepted mathematics will proceed one claim, one version and one human explanation at a time.