Tech Teardown 019 | openai/math: Repository Teardown of OpenAI Open Sourcing 722 AI Math Manuscripts All at Once

On October 6, OpenAI released the repository openai/math on GitHub, unleashing in one go the mathematical research results produced by an unreleased internal model: 722 manuscripts, 372 result families, 3.1 GB, 132,880 files, 9832 stars in two days (still rising), related HN discussions with over 1200 upvotes and more than 1400 comments, accompanied by the official blog post ‘Sharing AI progress in mathematics’ on the same day. It is not a collection of papers, but a three-piece set of ‘manuscript + formalization + verification tools’. The reading, verification, and controversies of this repository are almost entirely rooted in this three-layer structure. This article breaks it down into six aspects: what it is, why it is worth watching, structure and mechanism, numbers and boundaries, how to verify, and value judgment.

1. What It Is

openai/math is an AI math output repository: primary language Lean, Apache-2.0 license, three layers of content plus a manuscript map.

The first layer is preprints/, 722 directories, one research manuscript per directory, containing paper.pdf, LaTeX source files, citations, and build instructions. Directory names include a date stamp: the earliest is September 10—the exact day the Navier-Stokes result was publicly announced—the latest is October 5, and the public release was on October 6. The manuscripts were accumulated for nearly a month before being released all at once, and the timestamp of the first commit falls on the very day of the public release.

The second layer is lean/, the formalization library. Under OAI/ there are 24 subdirectories divided by subject, from Algebra to Topology, with 121,700 .lean files; it depends on mathlib4 and is locked to the specific commit d13f23b, with patches/ storing patches to the upstream—this library does not merely consume mathlib4, it has modified the upstream.

The third layer is reasoning_traces/, containing reasoning summary PDFs for 10 result families. The README claims them to be abridged summaries, but HN comments point out that a more accurate description is ‘excerpts of summaries’—not the original reasoning traces.

There are two top-level navigation files: CONTENTS.md, a 640 KB manuscript map, registering all 722 manuscripts one by one, each providing the title and a pointer to the conclusion; the 001, 003, 102, and 180 referenced below are entry numbers in this map; overview.pdf with source files, 323 KB, is an overview of all results. The repository is organized by ‘families’; a main result plus accompanying arguments, corollaries, and alternative proofs counts as one family, and the 722 manuscripts are grouped into 372 families—a considerable portion of the results are released together with alternative proofs or accompanying arguments, so when reading, it is more worthwhile to read by family than by individual paper.

II. Why It’s Worth Looking at Now

The first reason is the weight of the results list itself. The 722 documents are not 722 isolated problems; organized by families, it is more like a research archive; in CONTENTS.md, besides the heavyweight entries, there are also scattered the irrationality exponent of π, the Erdős-type quasi-polynomial bound for arithmetic progressions, the Kaplansky directly finite characteristic 2 counterexample, free group factor isomorphism, relativistic Vlasov–Maxwell, Mahler conjecture, and spontaneous magnetization of the quantum Heisenberg ferromagnet—stretching all the way from number theory and graph theory to mathematical physics. Let’s highlight four of the heavyweight ones.

No. 003, the Quasi-Riemann Hypothesis: the ζ function and all Dirichlet L functions have no zeros in the region Re(s)>7/8, accompanied by the uniform exclusion of Landau–Siegel zeros. The direction must be clarified first: the further to the right the zero-free region, the stronger the result; the human record is 11/12≈0.9167, and 7/8=0.875 is to its left—this is a lower bound independently advanced by the system on an old problem, not a record-breaking one.

No. 102, the Unique Games Conjecture (Khot, 2002), the manuscript provides a proof of its validity. This is an infrastructure-level proposition in theoretical computer science, with a large number of inapproximability results predicated on it; there are comments on HN (Hacker News) suggesting its weight is greater than some Millennium Problems.

No. 180, the Barnette Conjecture (1969): every finite simple cubic bipartite planar 3-connected graph has a Hamiltonian cycle. A 57-year-old open problem in graph theory; an HN user recounted spending months attacking this problem with the strongest model of the time, to no avail.

No. 001, the Milne Rationality Conjecture (for abelian varieties), with the same entry listing side-by-side a claimed proof of the special case of the Hodge conjecture for CM abelian varieties—we must stick to the exact claim: this is only a claim for a special case, certification by the Clay Mathematics Institute has not occurred.

The second reason is the form of the release. Previous public releases in AI mathematics have mostly been single-point claims; releasing 722 documents all at once, as an entire repository complete with a formalization layer and verification tools, is a form that is rare in itself. New ways to play with it have already emerged in the HN discussions: someone threw the entire repository to their own agent, asking it to answer the significance of each manuscript one by one—the scale of 722 documents has forced out a new way of reading.

3. Core Technical Mechanisms

The generation pipeline is stated in the README: the vast majority of results are produced by the same unreleased internal model following a fixed process; approximately 4000 problems were fed throughout the process, with each result consuming an average of 3 hours of thinking compute equivalent to ChatGPT Pro; the outputs were aggregated into families, and after passing the significance threshold, 722 remained. Two items are listed as exceptions outside the fixed process: the Riemann zeta zero-free region and the Hodge case of CM abelian varieties. The README does not elaborate on the differences, only stating that the paper on the zero-free region was manually edited for readability.

The organization of the formalization layer is worth a closer look. Under lean/docs/, each formalized result has a one-page document, clearly stating the scope of application, the corresponding paper, and the Comparator link. Taking No. 003 as an example again: the statement covers the ζ function, all Dirichlet L functions, and finite-order Hecke L functions over Q(√-3); the pole of the principal character at s=1 is explicitly excluded from the statement; constants are not given explicit values. What has been formalized and what has not are clearly delineated in the documentation—when reading this repository, read the docs first, then the code; these page-by-page explanations are the easiest entry point.

A reality check is needed specifically for the reasoning summary layer. 10 families are equipped with reasoning_traces, the README’s wording is abridged summaries, and HN discussions point out that these are actually “excerpts of summaries”. Compared to the thinking volume of “an average of 3 hours per result”, the reasoning materials the community gets are far from sufficient to reproduce the model’s reasoning path—for those who want to study “how the model thinks”, this is the most opaque layer of the repository.

The verification stratification is the most crucial part of the mechanism. formalization.yaml tallies 162 papers with formalized main results, accounting for just over 20% of the 722; the README’s exact words are that the results are at different verification stages and not all are equipped with Lean formalization, and it concedes that the unformalized parts may contain errors. In other words, the repository itself has labeled its credibility as a gradient: 162 are machine-checkable, while the remaining 560 are human-readable claims.

4. Numbers and Boundaries

The full tally of numbers: 722 manuscripts, 372 families, 162 formalizations, 132,880 files, 3.1 GB, approx. 4000 problems fed, an average of 3 hours per result, 9832 stars in two days; the Lean repository has 24 subject subdirectories, 121,700 .lean files.

Four boundaries are outlined.

First, do not get the direction backwards. 7/8 is weaker than 11/12; the AI’s result for the zero-free region does not surpass humanity. Writing it as breaking a record is the most common mistake on this topic; get the direction wrong, and the credibility of the entire piece is compromised.

Second, formalization does not mean error-free. The prerequisite for Lean verification is that the theorem statements are correctly translated—what the machine checks is the statement in the code, not the Chinese or English conclusion in the paper. The highly upvoted questioning on HN (Hacker News) lands exactly here: spanning 24 subjects, the translation of every single statement deserves human review; the fact that constants in document 003 are not given explicit values is exactly the kind of detail such checks must scrutinize; some directly predicted it would fail, while the respondents pointed out that the README already concedes that the unformalized parts may contain errors.

Third, release does not equal certification. The blog title uses ‘sharing’ not ‘solving’; neither Clay certification nor peer review has occurred; the paper is authored by OpenAI, with no human reviewer credited. The debate on HN between GitHub and arXiv also arises from this: some praised the GitHub release for breaking the paywall, while mathematicians retorted that mathematical results inherently go to arXiv, and the archival value of a repository is not isomorphic to that of a paper.

Fourth, for the compute metric, look behind the scenes; for the star count metric, look at the audience. 3 hours is an average metric; someone on HN dug up AlphaZero’s old record—the ‘4-hour superhuman’ was actually 4 hours multiplied by 5000 TPUs—reminding us that expressions like ‘3-hour ChatGPT Pro equivalent’ require asking about the total volume behind the scenes; while the 9832 stars in two days measure attention, not correctness—the repository itself marked the 722 manuscripts as verification gradients, and community re-examination has only just begun.

5. How to Run, Who Can Play

You can verify without running the model; this is the most solid part of the repository’s design. lean/README provides the Comparator workflow: first install the three components comparator, landrun, and lean4export, run lake update to pull dependencies, run lake exe cache get to fetch the mathlib4 cache, and then execute lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json—to run a cross-check against the formal statement of No. 003. ComparatorChallenges/ contains the official preset challenge list; following this workflow, you can spot-check item by item. To compile the full library, the README specifically warns that the default vm.max_map_count limit on Linux might not be enough, and provides a workaround using CMake -DMMAP=OFF plus GLIBC_TUNABLES—the fact that a repository is so large that the official needs to specifically write compilation pitfall avoidance instructions is precisely a footnote to its sheer volume.

Let’s address three types of people. Those working in Lean and formalized mathematics: 162 formalized results with accompanying papers and documentation, plus the mathlib4 lockfile and patches, are assets you can directly read and verify hands-on; they are also ready-made samples for observing “how AI output lands in Lean.” Those in theoretical computer science: Whether the Unique Games manuscript ultimately holds up or not, it is worth reading line by line—the landscape of inapproximability it affects is so vast that every step of verifying its conclusions will be repeatedly cited by the academic community. Those doing model evaluation: The entire screening pipeline of feeding 4000 problems, family aggregation, and significance thresholds, along with the cost metric of 3 hours per result, constitutes a rare, first-hand methodological asset.

For those who just want to look around, the barriers to entry are disk space and patience: a 3.1 GB clone, plus a full library compilation that your machine might not be able to handle; for those who don’t want to install anything, start by reading the 323 KB overview.pdf in the top-level directory—in twenty minutes you’ll have a bird’s-eye view of the entire repository’s results, and then you can decide which subject directory to dive into.

6. Value Judgment and Who It Is For

The sample has high value. It transforms “AI doing math” from a single-point claim in press releases into a public repository that can be inventoried, spot-checked, and machine-reverified. The number 162 is particularly crucial: even if everything else is open to doubt, the formalized statements of these 162 papers are hard content that the community can independently verify. The stance expressed by Fields Medalist Terence Tao on Mastodon (reposted by HN) aligns with this same direction: he hopes AI can explain its results to human mathematicians, and believes AI can make positive contributions in exposition and community building.

The productivity value varies depending on the person. For researchers in mathematics and theoretical computer science, this is a must-know existence, if only to determine whether their own topics have been scooped—on HN, PhD students have already expressed anxiety about “getting hit by the 722 papers while halfway through writing a paper,” and empathetic replies advised embracing the frontier and not pasting unpublished research text into AI. This sentiment itself is also an industry variable. For the engineering side, the verification toolchain and documentation for avoiding compilation pitfalls serve as ready-made references for large Lean projects. For those who only want conclusions, a reminder: there are no conclusions here, only claims at different stages of verification.

The blog additionally promises to fund a series of workshops, conferences, and dedicated projects to help the mathematics community understand the major results produced by AI, and states that it is advancing the responsible release of the models that produce these results; the README also mentions exploring community-hosted repositories. To conclude with a bit of background: the ten-problem Lean in August, and the Fields Medalist statement and advisory group proposal in September, constitute the external background for this release method; the expansion of the critical aspects is covered in the same-day trending post, and will not be reiterated here.

One-sentence judgment: the historical position of openai/math does not depend on how many of the 722 items ultimately hold up, but rather on it being the first time the output of AI mathematics has been placed onto a track where human mathematics can inspect it item by item—the star count is OpenAI’s, but the right to inspect item by item is the community’s.

References

• Main repository: github.com/openai/math (after local cloning, compared item by item: README, CONTENTS.md, lean/ directory, formalization.yaml, git log; no builds were executed)
• OpenAI blog “Sharing AI progress in mathematics” (2026-10-06)
• HN story 49984923 (as of 2026-10-08, over 1200 upvotes and 1400+ comments; Terence Tao’s statement and the advisory group’s proposal are both cited via HN, original texts not verified word-for-word)
• Star count 9832★ is the figure as of 2026-10-08, and is still rising