Every number the atlas states in a sentence, with what it counts, the rule that counts it, whether it was computed or reported, and who it is credited to. Each one opens the records behind it.
Statement Map, the program that collects Atlas’s source records, computes each number and saves the items counted. A total supplied only by a source is marked as reported. If inputs are missing, the page says so instead of displaying zero.
Unless a number names its own credit, its records are credited to: Will Cook, OpenAI Math Atlas; source manuscripts and Lean quotations credited to OpenAI.
372
Counts families. Computed from the records.
Rule. Each family number in OpenAI’s catalogue, counted once.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
17
Counts disciplines. Computed from the records.
Rule. Each discipline the catalogue groups families under, in the catalogue’s order and with its names.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
719
Counts papers. Computed from the records.
Rule. Each paper the release lists as current.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
3
Counts papers. Computed from the records.
Rule. Each paper the release lists as withdrawn.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
27
Counts papers. Computed from the records.
Rule. Each paper the release lists as an earlier edition of a later paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
416
Counts Lean statements. Computed from the records.
Rule. Each Lean statement with its configuration. One Lean statement may name several theorems.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
189
Counts Lean statements. Computed from the records.
Rule. Each Lean statement that names at least one theorem the release lists as a main result.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
200
Counts listed main results. Computed from the records.
Rule. Each main result the release lists, counted once per entry, even when two entries share a name.
Credit. Computed from OpenAI’s release at the pinned commit.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
536
Counts theorems named by configurations. Computed from the records.
Rule. Each theorem a configuration names, counted once for each pair of solution file and theorem name. Every configuration that names it is kept in the records.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
242
Counts families. Computed from the records.
Rule. Each family whose Lean scope note in the release links at least one Lean statement. A link says the two are associated; it does not say how much of the family’s claim the Lean states.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
339
Counts papers. Computed from the records.
Rule. Each current paper that a Lean scope note in the release names as an accompanying paper, whatever part of the paper the Lean covers.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
65
Counts definitions left for the solution, one per configuration. Computed from the records.
Rule. Each definition a configuration leaves for the solution to supply, counted once per configuration, repeats included. These are what a configuration lists; they say nothing about what a proof actually uses.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
10
Counts Lean statements. Computed from the records.
Rule. Each Lean statement whose text defines no local vocabulary and imports nothing from outside Mathlib.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
11
Counts Lean statements. Computed from the records.
Rule. Each Lean statement whose text defines no local vocabulary.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
405
Counts Lean statements. Computed from the records.
Rule. Each Lean statement whose text defines at least one piece of local vocabulary.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
2
Counts Lean statements. Computed from the records.
Rule. Each Lean statement that imports at least one file from outside Mathlib.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
1
Counts Lean statements. Computed from the records.
Rule. Each Lean statement whose text declares an axiom. This reads the text; it does not trace what a proof depends on.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
10,828
Counts local definitions. Computed from the records.
Rule. Each local definition found by reading the text of the Lean statements, leaving out the theorems and lemmas themselves. Lean did not elaborate these files for this count.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
13
Counts local definitions per Lean statement. Computed from the records.
Rule. The median number of local definitions per Lean statement, counting statements with none. With an even number of statements it is the average of the two middle values.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
1,212
Counts local definitions per Lean statement. Computed from the records.
Rule. The largest number of local definitions in one Lean statement. The records list every statement that reaches it.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
Atlas retains two lists of citations between papers. Statement Map’s current extraction finds 586 ordered pairs of citing and cited papers. Atlas’s earlier extraction finds 579; it lacks the additional pairs found by Statement Map. Neither list is claimed to contain every citation.
586
Counts ordered pairs of papers. Computed from the records.
Rule. Each pair of papers in which one cites the other, counted once in each direction. A citation records that one paper cites another; it says nothing about how the cited result is used.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
579
Counts ordered pairs of papers. Computed from the records.
Rule. Each pair of papers in which one cites the other, counted once in each direction, from the atlas’s own earlier extraction. A citation records that one paper cites another; it says nothing about how the cited result is used.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
386
Counts papers. Computed from the records.
Rule. Each current paper that cites at least one other paper in the release.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
381
Counts papers. Computed from the records.
Rule. Each current paper that cites at least one other paper in the release, from the atlas’s own earlier extraction.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
217
Counts papers. Computed from the records.
Rule. Each current paper that cites a paper in the release with no associated Lean statement, or the latest edition of one. Having no associated Lean says nothing about whether the result could be formalised.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
214
Counts papers. Computed from the records.
Rule. The same count from the atlas’s own earlier extraction: each current paper that cites a paper in the release with no associated Lean statement, or the latest edition of one.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
16,077
Counts pairs of a paper and a bibliography entry. Computed from the records.
Rule. Each reference key in a current paper’s bibliography that points outside the release, counted once per paper and key. Two keys grouped as the same work still count twice.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
11,019
Counts automatically grouped works. Computed from the records.
Rule. Each work outside the release cited by current papers, grouped automatically by DOI, then arXiv identifier, then title. No manual review of the grouping is recorded.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
An AI agent classified OpenAI’s note about what each Lean statement expresses. No human review of these classifications is recorded, so these counts describe drafts.
416
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement given a draft classification by an AI agent. The classifications have no recorded human review and do not establish that a Lean statement means the same thing as the paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
307
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement an AI agent’s draft classifies as stating a paper’s theorem as the paper does. Nobody has reviewed the draft.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
21
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement an AI agent’s draft classifies as stating part of a paper’s theorem. Nobody has reviewed the draft.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
28
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement an AI agent’s draft classifies as stating a consequence of a paper’s theorem. Nobody has reviewed the draft.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
24
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement an AI agent’s draft classifies as stating a weaker form of a paper’s theorem. Nobody has reviewed the draft.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
35
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement an AI agent’s draft classifies as stating a supporting result. Nobody has reviewed the draft.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
1
Counts Lean statements with a draft class. Computed from the records.
Rule. Each Lean statement an AI agent’s draft classifies as unclear from OpenAI’s note. Nobody has reviewed the draft.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
24
Counts families. Computed from the records.
Rule. Each family in which an AI agent’s draft finds no Lean statement that states a paper’s theorem as the paper does. The draft keeps its own date and has not been reviewed.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
10
Counts families. Computed from the records.
Rule. Each family in which an AI agent’s draft finds Lean statements of part of a paper’s theorem and none of a whole one. The draft keeps its own date and has not been reviewed.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
14
Counts families. Computed from the records.
Rule. Each family in which an AI agent’s draft finds Lean, but no statement of a paper’s theorem, whole or in part. The draft keeps its own date and has not been reviewed.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
55
Counts families. Computed from the records.
Rule. Each family in which an AI agent’s draft puts the family’s Lean statements in more than one class. The draft keeps its own date and has not been reviewed.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
Counts obtained by scanning the text of OpenAI’s Lean library at the source version shown here. Lean was not run to interpret or verify the files for these counts.
559
Counts items as the release reports them. Reported by the source; its members are not listed.
Rule. Each project folder in OpenAI’s Lean library that holds Lean files.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
122,458
Counts items as the release reports them. Reported by the source; its members are not listed.
Rule. The number of Lean files in OpenAI’s library, as the release reports it.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
230
Counts items as the release reports them. Reported by the source; its members are not listed.
Rule. Each project in OpenAI’s Lean library with at least one file named Model.lean. The next number counts the files.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
248
Counts items as the release reports them. Reported by the source; its members are not listed.
Rule. The number of Model.lean files in OpenAI’s library, as the release reports it.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
967
Counts declarations found in the text. Computed from the records.
Rule. Each definition of a proposition in a Model.lean file, found by reading the text. Lean did not build these files for this count.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
196
Counts projects. Computed from the records.
Rule. Each project whose Model.lean statements are linked to a family. This says nothing about the library’s other projects.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
5,548
Counts declarations found in the text. Computed from the records.
Rule. Each theorem or lemma in OpenAI’s library whose name contains the word ‘manuscript’, found by reading the text. Lean did not build these files for this count.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
12
Counts projects. Computed from the records.
Rule. Each project that holds one of those theorems. This says nothing about the library’s other projects.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
2
Counts declarations found in the text. Computed from the records.
Rule. Each of those theorems whose name is exactly the theorem a configuration names. A matching name says nothing about how much of the paper is proved.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
Counts of TeX blocks labelled as theorems, lemmas, definitions and other statement types, added across the current papers. These are source labels, not assessments that the statements are correct.
2,255
Counts environments. Computed from the records.
Rule. The number of theorem environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
12,397
Counts environments. Computed from the records.
Rule. The number of lemma environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
4,745
Counts environments. Computed from the records.
Rule. The number of proposition environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
1,267
Counts environments. Computed from the records.
Rule. The number of corollary environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
555
Counts environments. Computed from the records.
Rule. The number of definition environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
583
Counts environments. Computed from the records.
Rule. The number of remark environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
21
Counts environments. Computed from the records.
Rule. The number of hypothesis environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
14
Counts environments. Computed from the records.
Rule. The number of claim environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
1
Counts environments. Computed from the records.
Rule. The number of question environments in the TeX source of each current paper, added up over the papers. These are counted separately from the statements the atlas lists for each paper.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
Reports by people and groups outside OpenAI. A finding is a report, not a judgement by the atlas.
372
Counts credited records. Computed from the records.
Rule. Each independent project or body of work credited by Atlas. Recording a reported problem does not establish that the report is correct.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
671
Counts credited records. Computed from the records.
Rule. Each report from those projects or bodies of work credited by Atlas. Recording a reported problem does not establish that the report is correct.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
371
Counts distinct credited names. Computed from the records.
Rule. Each distinct name or handle credited across those efforts, as written. The atlas has not confirmed who is behind each name.
The complete list of counted items and their sources is available as JSON, a machine-readable text format: Open the count’s source records
OpenAI’s reported figures and the atlas’s related counts, with the measure and source for each.
OpenAI’s figure
“719 manuscripts organized into 372 families”
The atlas’s count
719 papers in 372 families The records
OpenAI’s figure
“top-line results formalized to 300 / 719 = ~42%”
The atlas’s count
The atlas counts 339 current papers listed as accompanying papers in family notes that link a Lean statement, whatever part of the paper that Lean statement covers. OpenAI’s figure counts formalised headline results. The records
The release withdrew 3 papers. Their notices are quoted in full.
The proof relies on an adaptation of the flawed stabilization-trace construction in Algebraicity of Weil classes on split abelian eightfolds. The sign error in that construction prevents the required signed-double-point cancellation. The resulting gap leaves this paper’s claimed algebraicity theorem unproved.
This withdrawal concerns the proof; it does not assert that the mathematical statement is false.
Withdrawn on October 6, 2026.
The proof contains a sign error in the stabilization-trace argument used to obtain negative double points. In the manuscript’s signed double-point convention, write $I(f_1)=-m$ with $m>0$. The proof assigns each reverse stabilization trace sign $+1$ and therefore claims that inserting $m$ such traces makes the signed count zero.
Accounting for the opposite source orientations of the two branches of the standard cusp gives sign $-1$ for each reverse trace in this convention. The resulting count is therefore
$$I_{\mathrm{new}}=I(f_1)-m=-2m\ne0.$$
The Eliashberg-Murphy cancellation theorem invoked at this step requires zero signed double-point count, so its hypothesis is not met. The subsequent oriented-surgery and embedded-brane construction is therefore unsupported, and the paper does not establish its claimed algebraicity theorem.
This withdrawal concerns the proof; it does not assert that the mathematical statement is false.
Withdrawn on October 6, 2026.
The proof relies on an adaptation of the flawed stabilization-trace construction in Algebraicity of Weil classes on split abelian eightfolds. The sign error in that construction prevents the required signed-double-point cancellation. The resulting gap leaves this paper’s claimed rational Hodge theorem for products of projective K3 surfaces unproved.
This withdrawal concerns the proof; it does not assert that the mathematical statement is false.
Withdrawn on October 6, 2026.
Withdrawals
In “Algebraicity of Weil classes on split abelian eightfolds” a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers. As a result, we have withdrawn the following three manuscripts:
- Algebraicity of Weil classes on split abelian eightfolds
- Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
- The rational Hodge conjecture for products of K3 surfaces
The withdrawn papers now carry notices explaining the gap and linking to the archived manuscripts.
Fixes
We have revised 14 other manuscripts with proof repairs, corrected statements, clearer hypotheses and dependencies, and one correction to an obsolete citation. The changes include:
- Lipschitz heights and Ashkin–Teller currents (4 manuscripts): repaired crossing, boundary-attachment, conditioning and convergence arguments, including additional work on the real-Lipschitz interface proof.
- Kähler minimal model programs and abundance (6 manuscripts): expanded positivity and contraction arguments and clarified which results are used as inputs, with their required hypotheses.
- Taming and hypersymplectic deformation (2 manuscripts): corrected the cone-equality claim in Taming implies compatibility, added a strict-inclusion example, and removed an unnecessary cone-comparison dependency from the hypersymplectic paper.
- Incompressible Box Transport and Finite Computation: revised the torus-projection and common-clock estimates.
- Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank: removed an obsolete introductory citation to a removed supporting manuscript.
Also, as a consequence of these fixes we updated 13 additional manuscripts to cite the revised editions of companion papers. These changes update references and version dates.
Additional Formalizations
We have added an additional 6 formalizations and 5 other additions covering supporting results. This brings the total percentage of top-line results formalized to 300 / 719 = ~42%.