Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

About the atlas

What it is

The Plectis Atlas is an independent guide to OpenAI’s mathematics release of 6 October 2026. OpenAI groups related papers into 372 families. Of those, 242 have statements written in Lean, software for writing mathematical statements and verifying proofs. Atlas provides reading pages for the papers, places Lean statements beside possible paper counterparts, and links independent assessments and proof-verification reports.

The essays behind the design

These essays shaped how the Atlas approaches explanation, credit and formal statements. Their authors are cited for their ideas; this does not imply endorsement or review of the Atlas.

  • Henry Cohn, in The technical debt of AI-generated mathematics, argues that a correct result nobody can follow leaves a debt for other mathematicians to pay, and that whoever publicises such work should make it understandable.

  • Silvia De Toffoli and Eamon Duede, in After Math, separate a valid answer, which a formal certificate can establish, from an intelligible solution that mathematicians can grasp, communicate and build on.

  • Bryna Kra, in Deep theorems were scarce and difficult, argues that theorem counts no longer show understanding, and asks that discovery, proof, formalisation and explanation each be credited.

  • Grant Sanderson, in If math is more than proof, asks that motivated explanations, which show why a result is true and why it was worth asking, earn the credit that proofs do.

  • A declaration posted by Terence Tao and first signed by 25 Fields Medallists, in A Severe Misalignment of AI in mathematics, warns that rushing AI systems at famous problems puts attribution and the human transmission of ideas at risk.

  • Daniel Litt, in A beginning for mathematics, argues that mathematics should be judged by human understanding, which makes the people who explain and teach it more necessary.

What the atlas does in response:

  • Each family page quotes OpenAI’s description of its result and links the paper statements that may express it. Every paper has a reading page.
  • Where the release includes a Lean statement, Atlas places it beside a possible paper counterpart and reports independent assessments of what it expresses.
  • Atlas names the groups that examined statements or ran proof-verification programs and describes what their reports establish.
  • Each paper’s references are listed. Earlier work can be credited at the relevant passage, and independent reports retain their authors, dates and sources.
  • Contributors can explain results, compare statements or propose corrections, with named credit and disclosed AI assistance.

Since the release

Three pieces published since the release bear on how the atlas words what it shows.

  • Thomas Hales, in What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI, a guest post on Terence Tao’s blog (9 October 2026), explains that Lean’s kernel check is the core safeguard, and that a person must still confirm that a formal statement and its definitions say what was intended. This is why every Lean statement here is shown whole, with who compared it with the paper and what they found.

  • Thomas Bloom, in Changes to the Erdős problems web site, a guest post on Terence Tao’s blog (6 October 2026), describes removing problem statuses and the count of solved problems from erdosproblems.com, in favour of neutral wording such as “it is known that”, with a source. The atlas follows the same discipline: it says what is recorded and by whom, and keeps no tally of results.

  • The Association for Human Mathematics, in AHM Statement on OpenAI’s October 6 Release of Mathematical Documents, reposted on Terence Tao’s blog (7 October 2026), sets out its view of the release and asks mathematicians to stop working with OpenAI. The atlas records it as one perspective on the release, and neither joins nor answers it.

None of these authors has reviewed or endorsed the atlas.

What the atlas adds to the release

OpenAI publishes 719 current papers as PDF and TeX, the typesetting source; 416 Lean statement files for its Comparator proof-verification program; a catalogue; and notes on what the Lean statements express. For each of its 372 families, Atlas adds:

  • a reading page for every paper, with links to individual theorems; incomplete conversions list what is missing, and the PDF remains the reference;
  • possible main theorems selected from shared wording, with links to their passages;
  • Lean statements beside possible paper counterparts, with the reason for each link and whether a comparison has been reviewed;
  • independent groups’ reports of running proof-verification programs on OpenAI’s proofs, credited and dated;
  • independent assessments of whether a family’s Lean statements express the result OpenAI describes in its catalogue, quoted in each group’s own terms;
  • reports of proofs in another proof assistant and exact calculations for finite claims;
  • citations between the release’s papers, with links in both directions;
  • forms for contributing an explanation, comparing statements or proposing a correction, with named credit.

How it is built

Scripts read release version fd4aeeb and extract catalogue entries, paper sources, bibliographies, Lean statements and OpenAI’s notes. Each generated page links to its sources. Paper reading pages are converted from TeX. KaTeX tests whether the formulas can be typeset, not whether they are mathematically correct. Incomplete conversions list what is missing; the PDF remains the reference. Contribution status comes from Atlas’s own records.

Statement Map, a program by Will Cook, collects the release’s statements, Lean files, independent assessments and contributions into versioned records. Atlas imports these records and computes possible paper matches from shared wording. Those matches are labelled as candidates; they are not reviews of mathematical meaning.

The imported records have generation identifier e44fe048bf34, format version statement-map-web/2, and exporter reader-projection/6 from Statement Map revision 67e96aef1d2c. Validation report dd59201ab979 records software tests at revision 0b445d5dd326. The site build rejects records that do not match this export’s version and file hashes. These tests validate the data format and consistency, not the mathematics. What each number counts, with its source records

Independence

Atlas is an independent project, not affiliated with or endorsed by OpenAI. It describes the release, quotes OpenAI’s claims and links reports about specific statements, proofs and calculations.

It is equally independent of every group whose work it credits: Carlos Toledo’s cert-machine, MathVet, Neal McBurnett’s openai-math-lean-tooling and Ben Knill’s openai-math-hol-cards. Each group’s findings are shown as their own, in their own terms, and none of them has reviewed or endorsed the atlas.

How this atlas was made

Will Cook built Atlas with AI coding agents under his direction. The repository contains the scripts that extract and count material from the recorded release version. AI-drafted assessments of what the Lean statements express are labelled as drafts with no recorded human review. Named comparisons with papers and reports of proof verification are recorded separately.

Review status

Atlas records source material, assessments and reports of proof verification. It does not provide peer review or endorse the release’s results. Each page names the reports it records and the claims those reports cover.

What the release’s README says about how it was made

OpenAI’s README records the following about how the release was produced:

  • “719 manuscripts organized into 372 families” README.md
  • “unreleased internal OpenAI model” README.md
  • “On average, each result used three hours of ChatGPT Pro thinking compute with that model” README.md
  • “posed approximately 4,000 problems” README.md
  • “top-line results formalized to 300 / 719 = ~42%” history.md
  • “the writeup for the Re(s) > 11/12 zero-free region for the Riemann zeta function was human edited for readability” README.md
  • Abridged reasoning summaries for 10 results, linked from those results’ pages here.

Related efforts

Other places where people are examining AI-generated mathematics.

Licence and attribution

Original Atlas code and documentation use Apache-2.0; contributed explanations use CC BY 4.0. Imported source material, KaTeX and font subsets retain their own terms. The website includes their notices and licence texts. Sources, credits and licence texts

How to cite

Use the citation below for the Atlas, with its revision or your access date. Also cite the original paper or outside report when relying on its result; a citation to the Atlas does not replace that credit. CITATION.cff

Will Cook. Plectis Atlas: OpenAI's mathematics release, read and checked. https://wcook04.github.io/plectis-atlas/. Describing openai/math at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb.

Author

Will Cook builds and maintains the atlas. His own work on Erdős problems, with its Lean proofs, is at Plectis. Plectis