Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Sources

Source records for the release, its outside assessments and public reports, with 671 findings attached to specific results. Software and font credits are listed below.

Atlas credits reports where they appear and links their sources. Original material retains its authorship and terms. A group’s proof-verification report, a statement extracted automatically from a paper, and a reviewed mathematical claim establish different facts; the page identifies which is being shown.

Attribution notice · Software and fonts · Citation metadata

Each entry is a public project, paper, post or organisation, described in the atlas’s words with a link to the original. Listing someone’s work does not mean they endorse the atlas. Add your work or correct an entry

Release and Atlas source records

openai/math

OpenAI, source version fd4aeeb, Apache-2.0

The catalogue, the 719 current papers in 372 families with their TeX sources and bibliographies, the 416 Lean statements and the Lean library, OpenAI’s Lean notes and its history file.

Plectis Atlas

Will Cook

Atlas’s extracted statements and possible Lean matches; AI-drafted assessments of what the Lean statements express; a source index of OpenAI’s Lean library; citations; and records explaining the published counts. The method follows Will Cook’s claim-faithful publication system for his Erdős problem corpus.

Software and fonts

These components are distributed with the website. The listed modifications describe how they were included; the original licences remain in force.

KaTeX 0.18.9

Khan Academy and KaTeX contributors · MIT

Typesets formulas in the browser; the paper builder checks formulas with the same version. Selected unmodified minified JavaScript, CSS and the auto-render and copy-tex extensions. Verified against the npm 0.18.9 distribution; the accompanying fonts are listed separately.

Licence text · Component source

KaTeX fonts bundled with 0.18.9

Design Science, Inc. (2009–2010); Khan Academy (2014–2018) · OFL-1.1

Formula glyphs used by KaTeX. Selected unmodified WOFF2 files from the npm distribution. Original embedded copyright, licence notices and reserved font names are retained.

Licence text · Component source

STIX Two Text 2.13 b171

The STIX Fonts Project Authors; Tiro Typeworks · OFL-1.1

Reading text. Subset, hints removed and renamed Plectis Serif; copied from the Plectis website font build.

Licence text · Component source

STIX Two Math 2.12 b168a

The STIX Fonts Project Authors; Tiro Typeworks · OFL-1.1

Mathematical symbols and the MathML font. Subset and renamed Plectis Math and Plectis MathML; copied from the Plectis website font build.

Licence text · Component source

Source Sans 3 3.052

Adobe; designed by Paul D. Hunt · OFL-1.1

Interface text. Subset, hints removed and renamed Plectis Sans; copied from the Plectis website font build. The fonts retain their 2023 Adobe copyright metadata.

Licence text · Component source

Records from independent groups

These sources supply the assessments and reports shown throughout Atlas. Each displayed report links to its original source.

cert-machine audit of openai/math

Carlos Toledo, snapshot 2026-10-11, Licence: MIT

Captured source revision 9814e4c06281 · Licence text

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family's challenge statements read against OpenAI's headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release's toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub's Linux runners (.github/workflows/openai-math-kernel.yml), one j

  • Proof-verification reports: Per challenge: the audit's Comparator re-run with both kernels, and for files with definition holes whether the displayed statement is proved.
  • Assessment of whether the Lean statements express the advertised result: Per family: whether the challenge statements state OpenAI's headline, with the gap and whether OpenAI's Lean note declares it.
  • Exact calculations for finite claims: Per family: finite parts of its papers decided by exact code written independently from each paper (lane F), with the verdict and what was decided.

Taken into the atlas

  • Data or source records: Its re-run verdict for each of the 416 challenges, with the held-definition checks for the ten files with definition holes (the Independent replay line on statement pages)
  • Data or source records: Its reading of each of the 242 families against OpenAI's headline, with the gap and whether OpenAI's note declares it (the readings of the scope on family pages)
  • Idea or design reference: Telling apart a gap OpenAI's note declares from one it does not (family pages)
  • Data or source records: Its exact decisions of the finite parts of 66 papers' arguments, including those whose objects were never published (family pages, under finite parts checked by exact computation)

Erdős problems in the OpenAI proofs

Thomas Bloom, snapshot 2026-10-11, Licence: none stated

Bloom's post lists the Erdős problems the release makes claims about, one section per problem, with the manuscript and any Comparator challenge. The atlas maps each manuscript to its family and links Bloom's problem pages; his remarks are linked, not copied. The post makes no judgement about novelty or attribution.

  • Erdős problems: The Erdős problems Bloom's post connects to a family, with links to each problem page.

Taken into the atlas

  • Data or source records: The problem numbers and short titles in his list, with the manuscripts and challenges each section links (facts, cited) (family pages)

HOL Light proof cards for openai/math

Ben Knill, snapshot 2026-10-08, Licence: MIT (code); CC BY 4.0 (explanatory prose)

Captured source revision 68a12280f84c · Licence text

Selected steps of eleven families proved again in HOL Light, independently of Lean, each card with negative controls that must fail; warm and cold runs recorded on 8 October. The author states that no card proves a headline theorem of the release. Compared first at release commit adc7f124 and updated by the author for fd4aeeb2.

  • Proofs of selected steps using HOL Light: Per family: what each HOL Light card certifies and how it relates to the release's Lean, in the author's words.

Taken into the atlas

  • Data or source records: What each card certifies and its relation to the release's Lean, quoted under CC BY 4.0 (family pages, under checks in another proof assistant)

MathVet fidelity review of openai/math

MathVet maintainers, snapshot 2026-10-10, Licence: Apache-2.0

Captured source revision 14c7f918cd33 · Licence text

An independent, model-assisted, pre-referee reading of each family's challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

  • Assessment of whether the Lean statements express the advertised result: Per family: MathVet's verdict on whether the challenge statements state the headline claim, with its review note.
  • Proof-verification reports: Per challenge: MathVet's own machine check.

Taken into the atlas

  • Data or source records: Its verdict and review note for each of the 242 families with Lean (the readings of the scope on family pages)
  • Data or source records: Its Comparator check for each challenge it ran (the Independent replay line on statement pages)
  • Idea or design reference: A published rubric and a protocol for measuring the error rate of statement-fidelity verdicts (the about and numbers pages)

Comparator runs of openai/math with build and memory measurements

Neal McBurnett, snapshot 2026-10-10, Licence: MIT

Captured source revision 824beb05b35e · Licence text

Each challenge's solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

  • Proof-verification reports: Per challenge: its Comparator verdict, check time and peak memory in this run.

Taken into the atlas

  • Data or source records: Its Comparator verdict for each challenge it has finished, with the check time and peak memory (the Independent replay line on statement pages)

OpenAI Math Tier List

Author not stated (public Claude artifact), snapshot 2026-10-11, Licence: none stated

The page's own judgements and counts, cited with credit; its prose is linked rather than copied. The page says its tiers assume each claim is correct as stated and that nothing on it is verified.

  • Kind of result: Proof, counterexample, algorithm or construction, as the page classifies each family.
  • Significance: How significant the page judges the result would be if it holds up, from 0 (highest) to 7.
  • Lean formalisations: The page's count of Lean formalisations per family.

Taken into the atlas

  • Idea or design reference: Classifying each result as a proof, counterexample, algorithm or construction, and its labels for all 372 families (family pages and the 'Proof or counterexample' map overlay)
  • Idea or design reference: Grading results by how significant they would be if they hold up, and its tier for each family (family pages and the 'Significance if it holds up' map overlay)
  • Idea or design reference: Its count of Lean formalisations per family (the published-counts reconciliation on the numbers page)

Findings and work cited from other people

Proof-verification reports, error reports, follow-up results, explanations and commentary, linked to the results they discuss and credited there.

OpenAI Lean companion repositories: NavierStokesAndEuler, ten-proofs, PrimeGaps186, LongGapsBetweenPrimes, cdc-lean

OpenAI, 2026-09-08, Linked. Licence: repository licence: Apache-2.0.

All five earlier OpenAI repositories holding Lean certificates for its maths announcements have issues and discussions disabled; NavierStokesAndEuler (created 8 September, 2,076 stars, 218 forks) has had no push since 10 September and ten-proofs (created 5 August, 213 stars) none since 5 August.

Covers family: 376

Cited by AGI

Will DePue, 2026-10-06, Linked. Licence: none stated.

An independent ranking of the human authors cited in the bibliographies of the 722 manuscripts, counting 9,399 authors and 16,576 attributed references at the 6 October commit, with each count traceable to a manuscript.

Area law and PEPS: provenance of imported OpenAI proofs (issue 8737)

LionSR, contributors, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

Issue opened 7 October (26 comments) setting provenance rules for formalising the release's two 24 September manuscripts in family 265 (a two-dimensional area law and polynomial PEPS approximation) in the TNLean tensor-network Lean library: copied, adapted and original code must be marked, with the Apache-2.0 notices retained.

1 finding on family: 265

mrnathanhumphrey-droid/openai-split-eightfold-gap: sign-convention check of Proposition 3.1

mrnathanhumphrey-droid, 2026-10-07, Linked. Licence: n/a.

Two small scripts examining Proposition 3.1 of the split abelian eightfolds paper: read in a single orientation convention, the stabilisation-trace cancellation count comes to minus 2m rather than 0, and the forward-trace double point is not orientably surgerable in every even dimension from 2 to 14.

1 finding on family: 032

Mutually unbiased bases: common states, completion, and extension obstructions

Hao-Yu Sun, 2026-10-08, Findings cited with credit. Licence: CC BY 4.0.

Studies common unbiased states and extension obstructions for mutually unbiased bases and cites OpenAI's computer-assisted theorem that dimension six has at most three such bases and its Fourier-certificate preprint giving at most five, explicitly without certifying the execution conditions or claiming community acceptance.

1 finding on family: 266

GTimG/QuasiRiemannTracker: dashboard of verified quasi-Riemann zero-free bounds

GTimG, records contributed by Nielstron, Akash Levy, Hailey Collet, Tim Gehrunger, others, 2026-10-09, Linked. Licence: repository licence: Apache-2.0.

Static site (gtimg.github.io/QuasiRiemannTracker) and pull-request workflow that ranks zero-free half-plane constants for all Dirichlet L-functions that passed a common Lean, Comparator and multi-kernel check.

2 findings on family: 003

OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb)

Jack McCarthy, 2026-10-09, Linked. Licence: repository licence: Apache-2.0.

A mirror of OpenAI's repository that removes definition_names from the ten Comparator JSON files that had a non-empty one, then repairs the challenges that broke (DefocusingNLS, SpinAngle, OccupiedOverlap) and gives ElementaryPositivity a theorem target.

14 findings on families: 103, 110, 145, 158, 169, 238, 297, 371, 374

Verification package for openai/math family 003, Uniform exclusion of Landau-Siegel zeros

Joseph M. Reilly, 2026-10-09, Linked. Licence: repository licence: Apache-2.0.

Independent replay of the family 003 SiegelZeros challenge with the official Comparator plus nanoda as a second kernel and the network blocked: both challenge theorems are accepted with only propext, Classical.choice and Quot.sound (Lean 4.34.1, Mathlib d13f23b7, Comparator v4.34.0, nanoda_lib 3a240721.

1 finding on family: 003

cjnott1999/barnette-conjecture: AI-assisted programme and verification of OpenAI’s proof

Cameron Nottingham, 2026-10-09, Linked. Licence: n/a.

Records a prior unsuccessful programme on Barnette's conjecture and, from 6 Oct, an independent verification of family 180: lake build succeeded (8,955 jobs), the solution model matches the challenge statement, only standard axioms are used, the 11-page paper was re-derived without finding an error, and an executable test built.

1 finding on family: 180

MathINsiD: bridge layer between bibliographic and formalised mathematics

Arnaud Mayeux, 2026-09-05, Linked. Licence: none stated.

An index of about five million records that runs from published papers to the Lean artifacts that formalise them, announced a month before the release and offered on 9 October as an answer to the request for a paper-to-Lean map, where a Lean maintainer replied it does not explain why OpenAI left the mapping out.

jkbennitt/math-release-atlas

Jason Bennitt, 2026-10-07, Linked. Licence: apache-2.0.

An unofficial static atlas of result families across three labs' public catalogues showing Lean status and community status with sources, committed largely by a coding agent.

4 findings on families: 002, 003, 032, 376

AlexSergy/MathOpenAi

Aleksandr Sergeev, 2026-10-10, Linked. Licence: none stated (README says upstream Apache-2.0).

A Russian-language static atlas giving plain-language explanations of 719 manuscripts, with a speculative set of 25 commercial product blueprints.

openai-wiles

ityonemo, 2026-10-09, Linked. Licence: none stated.

An audit of the withdrawn manuscript on Weil classes in the author's own proof checker, showing that the sign convention decides whether the stabilisation-trace step passes.

1 finding on family: 032

A proof of the Erdős--Gallai cycle decomposition conjecture

Jaehoon Kim, 2026-10-06, Findings cited with credit. Licence: CC BY-SA 4.0.

Proves the Erdos-Gallai conjecture that every n-vertex graph decomposes into O(n) cycles and edges (equivalently, Eulerian graphs into O(n) cycles, Hajos' conjecture up to a constant); the final section discloses extensive use of ChatGPT and Claude.

2 findings on family: 181

Changes (erdosproblems.com blog 9)

Thomas Bloom, 2026-10-06, Linked. Licence: n/a.

Announces a hiatus on new problem comments and proof claims, removal of open/solved statuses and of credit language, a priority for high-quality human expositions, and a rule that Lean formalisations should be registered on Palomar before the site links them.

Math 2.0 (Mathstodon thread and blog post)

Terence Tao, 2026-10-06, Findings cited with credit. Licence: none stated.

A four-part thread arguing that mathematics needs to value exposition, community building and new directions above being first to a solution.

OpenAI releases solutions to hundreds of problems (117 messages, 6-10 Oct 2026)

Lean community, 2026-10-06, Linked. Licence: n/a.

The most technical public thread on the release. It starts with a catalogue of where the Lean files live and who has mapped manuscripts to formal statements, then splits into: an AI-assisted audit of 405 Comparator statements (no false or vacuous statement found, about 10 weaker than the paper, several only partial), Alex.

11 findings on families: 002, 003, 004, 010, 030, 032, 103, 110, 143, 145 …

Sharing AI progress in mathematics

Hacker News readers, 2026-10-06, Linked. Licence: n/a.

The main discussion of OpenAI's announcement. Top branches: a commenter's 24-year personal history with Barnette's conjecture (claimed proved, family 180); an AI doomer asking others how to read the results; a commenter pointing to Proof Atlas, where the list claims to settle 90 of the top 500 open problems.

1 finding on family: 180

$\exists \mathbb{R} \subseteq \textsf{CH}$

Alex Meiburg, 2026-10-07, Findings cited with credit. Licence: CC BY 4.0.

Places the existential theory of the reals in the counting hierarchy (fourth level), in a 114-page text that the author says was discovered by ChatGPT in conversations ending 29 September and that is posted as a service because OpenAI released a very similar result with a slightly weaker bound on 6 October.

1 finding on family: 141

Abundance for threefolds in positive characteristic

Fabio Bernasconi, Jakub Witaszek, Zheng Xu, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves the abundance conjecture for threefolds in characteristic above 42 and says the preliminary draft was uploaded after OpenAI's list appeared, which claims abundance for threefolds in characteristic above 3.

1 finding on family: 035

Arxiv/2104.00502/BarkerSequence: barker_conjecture is true (issue 6917)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The circulant Hadamard manuscript implies every Barker sequence has length at most 13, but the release's Lean proof (EvenBarker) covers only even lengths; the odd-length classification is in the paper only.

1 finding on family: 179

Comment on the Birch and Swinnerton-Dyer results

David Ang, 2026-10-07, Linked. Licence: n/a.

A reading of the BSD results as completing the analytic rank zero and one cases by removing the assumptions of recent papers, with no Lean, and doing nothing for higher rank.

1 finding on family: 002

Comment on the deterministic Ramanujan graphs manuscript

Laura Monk, 2026-10-07, Linked. Licence: n/a.

A reading of the nonbipartite Ramanujan graph paper by a researcher who talks about this problem, judging that the title oversells what is an efficient deterministic algorithm.

1 finding on family: 178

Comments on the Grothendieck homotopy hypothesis manuscript

David Michael Roberts, 2026-10-07, Linked. Licence: n/a.

A category theorist identifies which version of the homotopy hypothesis is proved, calls it a closed problem of mainly historical interest, and advises treating only the formalised part of a partially formalised paper as trustworthy.

1 finding on family: 312

Commit comment asking for a channel to submit community materials

zoahdev, 2026-10-07, Linked. Licence: n/a.

A contributor asks how to submit a catalogue path checker (162 paper paths and 405 Comparator configurations resolve at adc7f12; structural only) and a Chinese reading guide, noting that external pull requests are restricted and Issues and Discussions are off.

ErdosProblems/1083: erdos_1083 is true (issue 6905)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The release's higher-dimensional distinct-distances manuscript gives at least c_d n^(2/d) distinct distances for d >= 3, which settles Erdős 1083; the release contains no Lean proof, so the suggested fix is to mark it solved and cite the paper only.

1 finding on family: 166

ErdosProblems/181: erdos_181 is true (issue 6906)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The hypercube Ramsey manuscript proves R(Q_n) <= C 2^n, exactly the formal statement; no Lean proof is in the release.

1 finding on family: 171

ErdosProblems/416: parts.ii has an explicit asymptotic formula (issue 6907)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The release does contain a Lean proof of the totient asymptotic (TotientAsymptotic challenge and UnconditionalMain), but stating the main term needs about 25 definitions (roughly 80 lines), so PR 6898 left part ii open; suggests copying the definitions from the challenge file.

1 finding on family: 024

Extensions of results in OpenAI/math (AI-assisted research drafts)

Rogerhu12, 2026-10-07, Linked. Licence: n/a.

Draft extensions of five release families, all stated to be unrefereed and unformalised: the irrationality exponent of log a for rational a (family 017), positive lower density for Artin primitive roots and Hecke zero-free regions over all number fields (029), modularity of elliptic curves over totally real and many CM fields.

Covers families: 017, 029, 030, 159, 172

HilbertProblems/5: the Hilbert-Smith conjecture is true (issue 6914)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The release manuscript proves the conjecture for second-countable groups acting on connected finite-dimensional manifolds; the Formal Conjectures statements do not assume second countability, so a reduction must be settled before marking them solved; no Lean proof is included.

1 finding on family: 304

Invariant Primes in Lubin-Tate Space and Hovey-Strickland at Every Height

Chenglong Ma, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves that the prime ideals of the Lubin-Tate ring stable under an open subgroup of the Morava stabiliser group are the height ideals, giving the Hovey-Strickland classification at every height.

2 findings on family: 311

Mathstodon: paper 312 proves a version of the homotopy hypothesis

John Baez, 2026-10-07, Findings cited with credit. Licence: none stated.

A mathematician who named the homotopy hypothesis notes that the release proves one version of it, that the hypothesis has easy and hard versions depending on how its terms are made precise, and that none of the papers will affect their work.

2 findings on families: 244, 312

OpenQuantumProblems/13: mutuallyUnbiasedBases_dim6 has answer 3 (issue 6918)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The release claims at most 3 mutually unbiased bases in dimension six by a computer-assisted argument, but its Lean proof gives only at most 5; the bound 3 and the computer-assisted exclusion of four bases are not formalised.

1 finding on family: 266

Points and their multiples on curves in powers of simple abelian varieties

David J. Smith, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves a finiteness statement for points whose multiples lie on curves in powers of simple abelian varieties and notes that OpenAI also announced a proof of Zilber-Pink for abelian varieties, as did independent forthcoming work of Barroero, Dill and Kuehne.

1 finding on family: 016

Positive bisectional curvature, Ricci mass, and the fundamental group

Ved Datar, Vamsi Pritham Pingali, Harish Seshadri, 2026-10-07, Findings cited with credit. Licence: CC BY 4.0.

Proves finiteness of the top power of the Ricci form for complete noncompact Kaehler manifolds with positive bisectional curvature, hence finiteness of the fundamental group (a case of a Yau-Yang conjecture).

1 finding on family: 338

Possible suggestions to "AI advisory group"?

Alexander Chervov with David White, others, 2026-10-07, Linked. Licence: n/a.

A wish-list thread for what to ask AI labs. David White's answer (+18) recalls the First Proof discussions and asks for prompts, scaffolding, retries, filtering and human feedback to be disclosed, full chat transcripts, access to the models, reporting of failures and problem-selection criteria, and preregistration. Chervov's.

Quantitative stability of optimal transport via regularization

Songbo Wang, Xiaozhen Wang, 2026-10-07, Findings cited with credit. Licence: CC BY 4.0.

Proves optimal Hoelder exponents for W2 stability of optimal transport for sources given by L^p changes of BV densities, and cites OpenAI's sharp one-third estimate for uniform sources on convex bodies as the closest earlier result; the optimal-transport result arose in a dialogue with OpenAI Codex, per the AI-use statement.

1 finding on family: 374

Significant Number of OpenAI Results Appearing to Resolve AIM Problems (issue 36)

JohnDriscollAcademic, 2026-10-07, Linked. Licence: n/a.

Lists nine correspondences between entries of an open-problem collection (not the American Institute of Mathematics) and release families, noting the exact statements and hypotheses were not cross-checked: 3D and 2D Anderson localisation (problems 015 and 016) with family 261, complete Crouzeix (023) with 325, relativistic.

3 findings on families: 087, 101, 102, 213, 261, 268, 325, 362

Stability of optimal transport on sub-Riemannian manifolds

Bang-Xian Han, Zhuo-Nan Zhu, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Studies stability of optimal transport on sub-Riemannian manifolds and records that the concurrent OpenAI preprint's three-atom example refutes a square-root conjecture from a 2026 paper of Letrouit on unstable optimal transport maps.

1 finding on family: 374

Strict correlation-dimension drop for quartic Salem Bernoulli convolutions

Guozheng Cheng, Xiang Fang, Xueqing Ma, Hongli Zhang, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves a strict correlation-dimension drop for Bernoulli convolutions of quartic Salem numbers and notes that OpenAI's manuscript, released during final preparation, settles singularity for every quartic Salem number in (1,2) but does not imply the correlation-dimension drop.

1 finding on family: 153

The Hellinger Conjecture for Antipodal Boolean Functions

Vu Khac Ky, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves the balanced Hellinger conjecture for antipodal Boolean functions (a single coordinate minimises the overlap throughout the noise interval) by a spectral argument and extends it to independent binary-input channels.

1 finding on family: 119

The Mathocalypse (Shtetl-Optimized)

Scott Aaronson, 2026-10-07, Findings cited with credit. Licence: none stated.

An enthusiastic overview by a complexity theorist listing the results that caught their eye, criticising the Association for Human Mathematics statement, and contrasting a lab that releases undigested proofs with one that pays authors to write them up.

12 findings on families: 032, 102, 103, 107, 283, 297

Transverse rational curves and the LeBrun--Salamon conjecture

Zhengyu Hu, Kefeng Liu, Xueyuan Wan, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves the LeBrun-Salamon conjecture (positive quaternionic-Kaehler manifolds of dimension at least 8 are Wolf spaces) using transverse rational curves; a remark says the core argument predates OpenAI's manuscript and differs from its smoothing-and-diagonal-jet approach.

1 finding on family: 062

Tweet: think in its general vicinity

Daniel Litt, 2026-10-07, Findings cited with credit. Licence: n/a.

A widely cited suggestion that mathematicians who dislike reading machine output can engage with a result by thinking in its general vicinity rather than reading it line by line.

Wikipedia/FlintCooksonHills: flint_hills_series_converges is true (issue 6909)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

With the release's mu(pi) = 2 (Lean proof of the exponent statement in PiExponent.lean) and Alekseyev's implication from mu(pi) < 5/2, the Flint Hills series converges; the release's own scope doc places the Flint Hills consequence outside the formalised statement.

1 finding on family: 017

Wikipedia/SurjunctiveGroup: gottschalk_surjunctivity_conjecture is false (issue 6919)

mo271, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

The two Kaplansky counterexample manuscripts give a non-surjunctive (non-sofic) group; the release's Lean covers the ring-theoretic statement and, for odd characteristic, injectivity and non-surjectivity of the cellular automaton as a plain map, but not continuity or shift-equivariance, so PR 6898 left it open.

1 finding on family: 197

Comments on the translational tile manuscript

Joseph Myers, 2026-10-08, Linked. Licence: n/a.

A summary of earlier comments by an expert on this tiling result: it gives weak rather than strong aperiodicity, does not discuss that distinction or the connected-tile literature, and a connected version needs no extra dimensions.

1 finding on family: 155

Geometrically Abelian Sections on Higher-Dimensional Varieties

Daebeom Choi, 2026-10-08, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Studies when sections of fundamental-group sequences of higher-dimensional varieties are geometrically abelian, motivated by OpenAI's claimed proof of the p-adic section conjecture.

1 finding on family: 019

Hyperkähler SYZ conjecture

Philip Engel, Mirko Mauri, 2026-10-08, Findings cited with credit. Licence: CC BY 4.0.

Proves the hyperkaehler SYZ conjecture (a nontrivial nef isotropic line bundle has sections defining a Lagrangian fibration); the authors say a largely complete human-written draft predates the release and that the structure of their proof looks similar to OpenAI's, which they have not yet examined carefully.

1 finding on family: 041

OpenAI withdraws three mathematical results

Hacker News readers, 2026-10-08, Linked. Licence: n/a.

Discussion of OpenAI's announcement on 8 Oct, by one of its researchers, of 6 new Lean formalisations, 19 modifications and 3 withdrawals.

1 finding on family: 032

OpenAI, the Partition Principle, and Mathematics

Asaf Karagila, 2026-10-08, Linked. Licence: none stated.

A set theorist's reading of the Partition Principle manuscript, finding the exposition unclear and the references uneven, and arguing that the release shifts verification work onto mathematicians.

1 finding on family: 244

Persistence of bounded trajectories in positively transverse reaction networks

Elisenda Feliu, 2026-10-08, Findings cited with credit. Licence: CC BY 4.0.

A reaction-network paper on persistence of bounded trajectories; it notes that the persistence, boundedness and permanence conjectures for weakly reversible networks are among the problems in the October 2026 OpenAI data release.

Covers family: 149

The Erdős similarity problem for null sequences with adjacent ratios bounded below

Kan Jiang, Lifeng Xi, 2026-10-08, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves a case of the Erdos similarity problem for null sequences whose adjacent ratios are bounded below, and cites both OpenAI's dyadic case (25 September) and its geometric case (5 October) of the Erdos similarity conjecture.

1 finding on family: 084

What should we tell our students?

Alvaro Lozano-Robledo, 2026-10-08, Linked. Licence: n/a.

Advice to students that keeps calm and carries on, with an afterword on the release listing the quasi-Riemann hypothesis, Goldfeld's conjecture, the Hodge conjecture for CM abelian varieties, Hilbert's tenth problem over the rationals and the rigidity conjecture as huge results, and reading the numbers as 4,000 problems.

Covers families: 003, 004, 006, 032

[Correction] JSP-000042 (Crouzeix): earlier human proofs of the scalar statement; independent Lean verification evidence (issue 4871)

Beltran12138, 2026-10-08, Linked. Licence: n/a.

Asks the Justin Sun Prize committee to list earlier human proofs of the scalar Crouzeix statement (Lorist and Schwenninger, arXiv 2608.03841, 4 August; Jin, 7 August; Luo, 28 August) next to OpenAI's complete-version claim, and offers the family 325 rebuild as supporting evidence for the entry's pending Lean verification note.

1 finding on family: 325

Confirm introducing history for exists_injective_not_dense_image_deriv_ne_zero (issue 44659)

grwtsk, 2026-10-09, Linked. Licence: n/a.

Provenance request opened in Mathlib: a downstream openai/math file (lean/OAI/Analysis/HotSpots/Riemann.lean) adapts a Mathlib theorem from Mathlib/Analysis/Complex/RiemannMapping.lean, keeps Yury Kudryashov's authorship and cites the exact Mathlib commit d13f23b7, but the source regions differ (2,852 bytes against 2,028).

Covers family: 369

What mathematicians should know about the Lean theorem prover

Thomas Hales, Terence Tao (host), 2026-10-09, Findings cited with credit. Licence: none stated.

A guest post on Lean's reliability that tells readers to audit whether the Lean statement and definitions match the intended meaning, which it calls much easier than checking the proof, and notes that Comparator helps.

grwtsk/openai-math: audit scripts and CI probes added to a fork

grwtsk, 2026-10-09, Linked. Licence: repository licence: Apache-2.0.

Fork with 61 commits adding path and encoding integrity scanners, theorem-closure receipt scanners and workflows named quasi-riemann-axiom-probe and kaplansky-witness-probe, each with hostile tests.

Covers families: 003, 197

mahrud/openai-math-comments

Mahrud Sayrafi, 2026-10-09, Linked. Licence: none.

A human-only public square for expert commentary with one bot-opened pull request per manuscript group, aimed at belief in correctness, context, exposition and credit.

4 findings on families: 063, 102, 194, 311

unique-games-short-proof: an 11-page self-contained proof and a 17-page faithful presentation of OpenAI’s Unique Games proof

Ariel Elboim, prepared with Codex, Claude, 2026-10-09, Linked. Licence: repository licence: NOASSERTION.

Two expository preprints (Zenodo DOIs) on OpenAI's proof of the Unique Games Theorem: a short proof using only Hastad's 3-LIN theorem, the Khot-Minzer-Safra Grassmann expansion theorem and Dinur-Steurer repetition as cited inputs, and a longer presentation following the original, with Lean check logs.

Covers family: 102

Why I don’t trust Lean code from AI

Asaf Karagila, 2026-10-10, Linked. Licence: none stated.

A second post saying they will not rely on AI-generated Lean at scale, while accepting that the formal statement of the Partition Principle is probably easy to get right, and asking labs to consult experts before releasing.

1 finding on family: 244

Swapnil-jain/mobius-x1: GF(2) Mobius transform below N log N

Swapnil Jain, 2026-10-11, Linked. Licence: n/a.

Preprint-stage construction of the GF(2) Mobius (zeta) transform in o(N log N) XOR gates for circuits with cancellation, with certificates and Lean 4 checks, adapting the architecture of OpenAI's family 130 DFT construction (eight-row network, three stages); not human refereed.

Covers family: 130

google-deepmind/formal-conjectures: 30 statement files cite openai/math (another desk covers its pull requests)

Google DeepMind, 2026-10-11, Linked. Licence: repository licence: Apache-2.0.

GitHub code search finds the string openai/math in 30 Lean files of the formal-conjectures statement library at the time of reading, including Erdős problems 3, 138, 172, 181, 184, 304, 371, 416, 431, 505, 508, 952, 968, 970, 978 and 1150, and the Falconer, Kaplansky, Irrational, Brennan, Borsuk and Sidorenko files.

Covers families: 073, 158, 159, 160, 164, 171, 181

Short Egyptian fractions (a simplified write-up)

Woett, 2026-10-10, Linked. Licence: none stated.

A human write-up, made with ChatGPT help, that substantially simplifies the short unit fraction result with an explicit constant far smaller than the manuscript's and derives the two related Erdős problems from it.

3 findings on family: 025

Jim Fowler index

Jim Fowler, 2026-10-06, Linked. Licence: none stated.

A human-built static index of the 722 manuscripts by subject with Lean checkmarks as listed upstream, page counts and full-text search of the LaTeX sources, linking to the Zulip statement review, whose README says no paper was read or classified by hand or by a model.

Valency Hub collection

Valency, 2026-10-06, Linked. Licence: works carry Apache-2.0 upstream.

A company hub that hosts the manuscripts as individual pages with view counts and search, used to promote its platform waitlist.

AgentLemma

Yassir Laaouach, 2026-10-07, Linked. Licence: links upstream Apache-2.0; none stated for the site.

A free catalogue of public AI maths releases across labs with search, filters by Lean availability and a discussion thread per paper.

Emergent Mind OpenAI Math Explorer

Matt Mazur, 2026-10-07, Linked. Licence: not stated.

A polished explorer with semantic search, a similarity map, an index of about 520 named problems, per-result pages with Lean scope notes and a model-written 'why it matters', and a roundup of reactions; the map and index are labelled as possibly erroneous.

Lance Fortnow TCS selection page

Lance Fortnow, 2026-10-07, Linked. Licence: none stated.

A complexity theorist's Claude-built page selecting theoretical computer science, combinatorics and other families with Lean badges, and a repository of two Claude-prepared expository rewrites of the Unique Games and L equals RL equals BPL proofs for human review.

Covers families: 102, 103

dwootton/openai-math-explorer

Dylan Wootton, 2026-10-07, Linked. Licence: none detected (README retains upstream licences).

A similarity map and reader for the 372 families with plain-language introductions, linked Lean source and a shared-reference view.

gokayfem/openai-math-explained

Gokay Aydogan, 2026-10-07, Linked. Licence: none.

An interactive 3D map with a 15-second model-made explainer video for each of the 372 results.

zlisto/openai_math: Paper Navigator

Tauhid Zaman, 2026-10-07, Linked. Licence: none stated.

A single-page navigator for browsing the manuscripts by subject and family, loading the PDFs from a public CDN mirror of the release.

foocker/openaimath: Chinese reading index of the release

foocker, 2026-10-08, Linked. Licence: none stated.

A Chinese-language reading index by subject and family with search, a self-hosted PDF reader, a checked English-Chinese terminology list of 85 terms and two narrated video explainers; its data snapshot is the 6 October commit.

2 findings on families: 002, 003

OpenAI Mathematics Preprints: Searchable Catalogue

Piotr Hajlasz, 2026-10-09, Linked. Licence: none stated.

A single large HTML file with full-text search over the 722 manuscripts, built by a mathematician with an AI model, whose MathOverflow request for ways to publicise it was voted down.

1 finding on family: 005

mrconter1/vibemathed

Rasmus Lindahl, contributors, 2026-07-27, Linked. Licence: repository licence: MIT.

Repository behind vibemathed.com (MIT code, created 27 July, 30 stars, last push 8 October).

3 findings on families: 003, 032

decalion89/chromatic-number-of-the-plane: Hadwiger-Nelson over number fields, rebuilding OpenAI’s formal proof

Sergi Galán, 2026-09-25, Linked. Licence: n/a.

Research repository with tests and a Lean workflow. It says OpenAI's non-constructive proof that the plane needs six colours gives chi(R^2) of 6 or 7, that no explicit finite unit-distance graph without a 5-colouring is known, and reports that the authors rebuilt the formal proof and checked in Lean that the ruler-and-compass.

1 finding on family: 158

Testing epimorphism onto the bicyclic monoid is $\mathsf{NP}$-complete

Luka Carroll, Murray Elder, 2026-10-06, Findings cited with credit. Licence: CC BY 4.0.

A group-theory paper (epimorphism testing onto the bicyclic monoid is NP-complete) whose v2 adds a remark that OpenAI's new quadratic Jacobsthal bound would sharpen one of its theorems, which the authors chose not to incorporate.

1 finding on family: 021

A Strong Dominability Criterion and an Oka Union Theorem

Yun-Heng Du, Bin Guo, Peng-Chao Wang, Song-Yan Xie, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Gives a strong-dominability criterion for a complex manifold to be Oka and an Oka union theorem; says it was directly inspired by OpenAI's proof that every complex K3 surface is Oka and extends that paper's Theorem 3.1 from surfaces to targets of any dimension, with an unpublished companion on rationally connected manifolds.

1 finding on family: 042

A relation between Mahler volume and flag number for convex polytopes

Martin Winter, 2026-10-07, Findings cited with credit. Licence: CC BY 4.0.

Proves vol(P) vol((P-P)^polar) <= flags(P)/(d!)^2 for convex polytopes, so that the Mahler conjecture implies Kalai's flag conjecture; includes a note that, if OpenAI's Mahler proof is correct, Kalai's flag conjecture follows.

1 finding on family: 087

Add a conjecture: the irrationality exponent of log 2 is 2 (issue 6899; PR 6923)

Kenta Kitamura, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

Proposes adding mu(log 2) = 2 to Formal Conjectures with the author's own proof note and Lean formalisation (repository KitaKen1/log2-irrationality-exponent), the PR reports only propext, Classical.choice and Quot.sound with no sorryAx.

1 finding on family: 017

Campaign: matrix multiplication exponent (omega)

Prove2Me, 2026-10-07, Linked. Licence: n/a.

Nine completed missions and none open, the newest dated 7 October 2026: a bound omega at most 2.25 over every field (4 theorems, 2 collaborators), which equals the release's 9/4 but the page does not mention OpenAI. Earlier completed missions cover published record bounds from 2.55 down to 2.371177 (an AlphaEvolve eighth-power.

1 finding on family: 107

Coloring Monomial Cayley Graphs: The One-Parameter Case

Jonathan Davidson, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Introduces monomial Cayley graphs to study how algebraic relations among unit directions affect the chromatic number of the plane; it cites OpenAI's proof that the plane has no proper 5-colouring and notes it implies the monomial-graph parameter reaches at least 6 for some finite r.

1 finding on family: 158

Hindman sums and products in Lean 4 (following OpenAI’s proof)

Yao Xu, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

Independent Lean 4 formalisation of the release's Hindman finite sums and products result (family 164), created 7 October with release v1.0.0, developed with Claude Code and Codex.

2 findings on family: 164

Lean proof that the matrix multiplication exponent is at most 9/4 over every field

Jeroen Zuiddam, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

Derived work of the release's Lean library (pinned to adc7f124) proving omega(F) at most 9/4 for every field, with 143 modules of which 99 are unchanged, 41 modified and 3 new; the change replaces the complex-only Fourier separation period by one valid in any characteristic.

4 findings on family: 107

Mattie/math: irrationality exponent preprints with Lean, extending the release’s method for pi

Ryan Matthew Casper, 2026-10-07, Linked. Licence: n/a.

Repository created 8 October with seven preprints (7 to 10 October), extending the release's irrationality-exponent-of-pi method: positive rational logarithms (exponent 2), nonzero rational arctangents, arctan(sqrt 2)/sqrt 2, log(3+2 sqrt 2)/sqrt 2, positive quadratic logarithms (at most 4), real and imaginary quadratic periods.

3 findings on family: 017

On the algebraic and analytic ranks of the twin-prime elliptic curve $y^2=x(x-2)(x-p)$

Ruihan Chen, 2026-10-07, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Treats the low-corank Birch-Swinnerton-Dyer implication announced in the OpenAI release as an explicit hypothesis and deduces equality of analytic and algebraic ranks, finiteness of Sha and the exact BSD leading term for the twin-prime curves y^2 = x(x-2)(x-p) in the residue classes p = 3, 5, 7 mod 8, leaving p = 1 mod 8 open.

1 finding on family: 002

Rectangular matrix multiplication from shared-leg entropy

Przemyslaw Uznanski, 2026-10-07, Findings cited with credit. Licence: CC BY 4.0.

Extends the shared-leg entropy analysis behind OpenAI's omega <= 9/4 to rectangular products, proving omega(1,k,1) <= 2 for k <= 1/2 (so the dual exponent is at least 1/2) and an O(n^2.5) running time for Zwick's all-pairs shortest paths in directed unweighted graphs; the note states it was produced with OpenAI Codex.

1 finding on family: 107

The centered logarithmic Brunn--Minkowski inequality

Yude Liu, Qiang Sun, Ge Xiong, 2026-10-07, Findings cited with credit. Licence: CC BY 4.0.

Proves the logarithmic Brunn-Minkowski and Minkowski inequalities for convex bodies with centroid at the origin, with equality cases; the introduction says the second author, assisted by GPT, obtained the centred characterisation after OpenAI released its symmetric log-Brunn-Minkowski proof.

1 finding on family: 091

eliottcassidy2000/math: THM-4568, the 9/4 growth lemma is exactly sharp

Eliott Cassidy, 2026-10-07, Linked. Licence: none stated.

A note in an AI-assisted research notebook proving that the profile properties behind the 9/4 matrix multiplication bound have a least element meeting the rank bound exactly at t = 3/4, so the argument cannot give an exponent below 9/4.

1 finding on family: 107

feat(Other): mark residual finiteness of hyperbolic groups as solved (PR 6921)

homeowmorphism, 2026-10-07, Linked. Licence: repository licence: Apache-2.0.

Merged on 8 October (06:49 UTC). Marks both open questions in Other/HyperbolicGroupsResiduallyFinite.lean as research solved with answer False, on the strength of the release's torsion-free hyperbolic group that is not residually finite. No formal_proof link is added because the release defines hyperbolicity by thin geodesic.

1 finding on family: 252

integer-mult-bounds

Douglas Colkitt, 2026-10-07, Linked. Licence: Apache-2.0.

A community repository, maintained with AI assistance, that improves the conditional exponent in OpenAI's integer multiplication result through reviewed pull requests with exact certificates.

2 findings on family: 109

matrix-multiplication-all-fields

selanavot, 2026-10-07, Linked. Licence: Apache-2.0.

A fork that extends the matrix multiplication exponent 9/4 argument from the complex numbers to every field, with a Lean proof that the author says passes Lean and Comparator.

1 finding on family: 107

snaky-15x15 and the playable Snaky site

gotrevor, 2026-10-07, Linked. Licence: Apache-2.0.

A certificate, checker and Lean proof that the first player wins Snaky on a 15 by 15 board, plus a site where a reader plays the losing side; the author says the strategy came from a separate search and AI help.

1 finding on family: 187

Hierarchical Melnikov Realization: Logarithmic Factor Improvement to Hilbert Number Lower Bounds

Chaoyang Qin, Xiaoming Sun, 2026-10-08, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Improves the known lower bound for Hilbert numbers H(d) by a factor of log d, to order d^2 (log d)^2, with a Lean 4 certificate (Zenodo archive cited in the paper); the authors say OpenAI's finiteness claim for H(d), released on 6 October, is independent of their lower-bound work.

1 finding on family: 143

Hodge conjecture formalisation and a CM abelian variety challenge

Paul Lezeau, Jack McCarthy, Abhijit A J, 2026-10-08, Linked. Licence: none stated.

After the release, members of the Formal Conjectures effort agreed to reuse their Hodge conjecture formalisation to state, as a challenge file, the rational Hodge conjecture for CM abelian varieties, which OpenAI had not formalised.

Covers family: 032

Mean dimension and radius of comparison

George A. Elliott, Zhuang Niu, 2026-10-08, Findings cited with credit. Licence: CC BY 4.0.

Extends the radius-of-comparison result from the integers to minimal free actions of discrete amenable groups with the uniform Rokhlin property and comparison of open sets, proving rc = (1/2) mdim, and the same for simple AH algebras with diagonal maps.

1 finding on family: 302

Slightly improved zero-free half-planes for the quasi-Riemann hypothesis

Baiying Liu, 2026-10-08, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Tunes the two parameters in OpenAI's argument for the uniform 7/8 zero-free half-plane (finite-order Hecke L-functions over Q(sqrt(-3)), hence Dirichlet L-functions) and improves the constant to about 0.874975, then to about 0.874957, with the new constants formalised in Lean 4.

1 finding on family: 003

Strict Hausdorff-dimension drop for Quartic Salem Bernoulli convolutions

Guozheng Cheng, Xiang Fang, Xueqing Ma, Hongli Zhang, 2026-10-08, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Follow-up by the same authors proving a strict Hausdorff-dimension drop for quartic Salem Bernoulli convolutions, building on their correlation-dimension paper and citing OpenAI's family 153 manuscript.

Covers family: 153

Swapnil-jain/integer-mult-kappa

Swapnil Jain, 2026-10-08, Linked. Licence: apache-2.0.

A parallel series of eleven numbered conditional bounds for integer multiplication that builds on the community repository and adds Lean-checked finite certificates, written with Claude.

1 finding on family: 109

Tiling 3D by Translates of a Single Polycube is Undecidable

Erik D. Demaine, Stefan Langerman, 2026-10-08, Linked. Licence: arXiv non-exclusive distribution licence 1.0.

Proves that deciding whether a single connected polycube tiles 3-space by translation is undecidable, by adapting the cyclic encoding from OpenAI's three-dimensional aperiodic tile to the Greenfeld-Tao two-prime Sudoku construction.

1 finding on family: 155

argonaut-math-quasi-riemann-boundary

Argonaut-Math, 2026-10-08, Linked. Licence: none stated.

A paper and Lean sources claiming a refinement of the quasi-Riemann zero-free boundary from 7/8 to 3499999/4000000.

1 finding on family: 003

hyperbolic-group-not-sofic

Apsiape, 2026-10-08, Linked. Licence: none stated.

A paper in a public repository that claims the hyperbolic group which OpenAI shows is not residually finite is also not sofic, pointed out by a topologist the day after the withdrawals.

2 findings on family: 252

openai/math repository: state check on 2026-10-11

OpenAI, 2026-10-08, Linked. Licence: repository licence: Apache-2.0.

No commit has landed since the merge of pull request 1 (fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb, 2026-10-08T05:20:00Z); there are three commits in all, two branches, no releases or tags, and issues and discussions are disabled.

1 finding on family: 032

shea256/fourier-transform-below-nlogn

Ryan Shea, 2026-10-08, Linked. Licence: apache-2.0.

A research draft, LaTeX source and verifiers extending the community integer multiplication network to the exact discrete Fourier transform, with a file auditing its dependencies.

2 findings on family: 130

MaxSNP-completeness and APX-completeness of MAX-3-SAT in Lean 4 (PALOMAR-2026-10-09-000010)

Robert D. Barish, 2026-10-09, Linked. Licence: n/a.

A Lean proof of the PCP theorem and its approximation consequences that vendors the closure of the release's Unique Games formalisation: 194 files, about 75,000 lines, adapted to the module system and to a newer Lean toolchain, including an opaque wrapper so that the nanoda checker does not unfold one large constant.

1 finding on family: 102

exact-dft-power-saving

danadran01, 2026-10-09, Linked. Licence: none stated.

A repository claiming a Lean-verified exponent saving for the exact discrete Fourier transform far larger than the manuscript's, extending OpenAI's algorithm and formalisation.

1 finding on family: 130

qrh-debruijn-newman

DrMurphyIsIn, 2026-10-09, Linked. Licence: none stated.

A Lean 4 repository describing a kernel-checked bound of 9/32 on the de Bruijn-Newman constant derived from the quasi-Riemann result and judged by Comparator.

1 finding on family: 003

wiggums-proof-loop

offline-ant, 2026-10-09, Linked. Licence: Apache-2.0.

A repository that shortens OpenAI's Unique Games Lean proof from about 151,000 to about 114,000 lines with an agent loop, keeping the statement and re-checking the result.

1 finding on family: 102

417 (a short write-up deriving a bound from the Erdős 416 result)

donteatllamas, 2026-10-10, Linked. Licence: none stated.

A short write-up, first generated by AI and then edited by the author to be human-readable, that derives an explicit bound of about 2.195 on the limit superior of a ratio in Erdős problem 417 from the totient asymptotic of the release.

1 finding on family: 024

Add three variants of Erdős Problem 952 (issue 7091)

Kenta Kitamura, 2026-10-10, Linked. Licence: repository licence: Apache-2.0.

Proposes three Gaussian-moat variants marked research solved, the first being the release's uniform Gaussian moat theorem (Bounded-Step Walks on Gaussian Primes) for which, the issue says, OpenAI provided the original Lean formalisation and the author supplied Lean proofs of all three.

1 finding on family: 028

Follow-ups to the OpenAI mathematics release (papers, sources and Lean ancillary files)

Jizhou Guo, 2026-10-10, Linked. Licence: repository licence: MIT.

Collection of single-author follow-up papers dated 8 to 10 October, pinned to commit adc7f124, including a zero-free half-plane for Hecke L-functions of nonzero angular type extending the quasi-RH cubic-theta method, hot spots for convex planar domains deduced from the release's hot spots paper, Liouville-sign Goldbach results.

2 findings on families: 003, 007, 011, 369

akashlevy/qrh: zero-free half-planes below 7/8 (10499/12000) and a 23/24 zeta proof

Akash Levy, 2026-10-10, Linked. Licence: n/a.

Research log and Lean formalisations from 8 to 10 Oct: a weighted-numerator proof of the exact bound 10499/12000 (about 0.874917), merged into the tracker as its best framework-verified record that day, and a separate 'shortest verified' proof that zeta has no zeros for Re s > 23/24, 121.5k lines of code and 72% smaller than.

1 finding on family: 003

shea256/matroid-prophet-inequality: a sharper one-sample matroid prophet guarantee (family 111)

Ryan Shea, 2026-10-10, Linked. Licence: repository licence: Apache-2.0.

Living paper on family 111. The latest certificate is C = 8003458533570087953 / 16807475946150704657203200000, above 51/50 times 2^-31 and about 1.15 times the previous 7/4 times 2^-32; the initial announced result was above 2^-36. It is written proof with same-agent verification and no independent review or formalisation.

1 finding on family: 111

Campaign: Integer Multiplication Below n log n

Prove2Me, 2026-10-11, Linked. Licence: n/a.

Campaign turning improved exponents for integer multiplication into complete Lean proofs, building on Harvey and van der Hoeven, the release's family 109 manuscript (which claims kappa = 2^-182) and later community constructions.

1 finding on family: 109

Formal Conjectures: mark problems solved in the OpenAI math release and link formal proofs

Moritz Firsching, anxkhn, Paul Lezeau, 2026-10-11, Findings cited with credit. Licence: none stated.

A human-reviewed pull request that links twenty-nine OpenAI Lean theorems in twenty-five files to Formal Conjectures statements after source inspection, recording six differences between the two statements, merged four days after the release.

28 findings on families: 005, 012, 013, 020, 021, 024, 025, 026, 028, 047 …

Leiden Declaration on Artificial Intelligence and Mathematics

Leiden Declaration working group, 2026-06-02, Linked. Licence: n/a.

Community declaration drafted after a September 2025 Lorentz Center conference, covering plausible but incorrect proofs, attribution and premature public claims, with recommendations on disclosing tool use, keeping humans responsible, insisting on peer review and supporting public computing.

VibeMathed: math problems solved with AI

VibeMathed, 2026-07-20, Linked. Licence: n/a.

Volunteer-run, community-curated tracker of open problems solved fully or partly with AI, with a resolution status, a Lean-verification tier, an AI-contribution tier and a 0 to 100 significance score, and a CC BY 4.0 dataset.

7 findings on families: 032, 034, 067, 076, 209, 240, 347

A Severe Misalignment of AI in Mathematics

Organisers of mathandai.org, 2026-09-11, Linked. Licence: n/a.

Open declaration arguing that AI companies' use of famous open problems as benchmarks harms mathematics, attribution and the human transmission of ideas, and calling for urgent action from mathematicians, AI developers and society.

Announcing the Advisory Group on Mathematics and Artificial Intelligence

Terence Tao (host), 2026-09-21, Linked. Licence: n/a.

Announces the group, its members and independence from AI companies, says it formed after OpenAI approached some members about an external advisory board, and says its first task is advising OpenAI on releasing a large number of significant results from an internal model.

Hexagon: a repository for research in the mathematical sciences and theoretical computer science

Hexagon, 2026-09-28, Linked. Licence: n/a.

Beta repository where each deposit is screened automatically and by a human moderator (acceptance is not a judgement of correctness), AI systems cannot be listed as contributors, Lean files are not accepted directly but can be linked from mathlib, Palomar, prove2.me or TauCeti, new accounts get one deposit per UTC day.

10 findings on families: 003, 005, 030, 084, 092, 158, 167, 198, 199

Responsible Release of AI-Generated Mathematics (AGMAI general guidelines)

AGMAI, 2026-09-29, Linked. Licence: n/a.

Nine-member independent group (Charles, De Lellis, Gowers, Hairer, Srivastava, Tillmann, Vakil, Witten, Wood) sets out release norms informed by over 600 survey responses: cite related prior ideas, write papers in conventional style, deposit in a lab-independent repository that allows comments, publish model, prompts.

Advisory Group on Mathematics and AI: guidelines and statement on the release

Francois Charles, Camillo De Lellis, Timothy Gowers, Martin Hairer, Nikhil Srivastava, Ulrike Tillmann, Ravi Vakil, Edward Witten, Melanie Matchett Wood, 2026-10-06, Findings cited with credit. Licence: none stated.

The independent advisory group hosted at the Institute for Advanced Study published general release guidelines on 29 September (formal links between natural-language and formal versions, community-hosted repositories with comments, disclosure of AI use) and a statement on 6 October that it does not endorse or judge the results.

Hexagon (new repository for LLM-assisted results)

Ben Antieau, 2026-10-06, Linked. Licence: n/a.

Announces Hexagon, a citable, community-maintained repository at hexagonmath.org for results produced with LLMs, run by a Delaware non-profit with a board of Abouzaid, Charles, Kra, Savitt and Williams and an advisory board including Buzzard, Mathew, Schmitt, Sigurdsson, Srivastava, Vakil and Ward.

Sharing AI progress in mathematics

OpenAI, 2026-10-06, Linked. Licence: n/a.

OpenAI's announcement says it is releasing results from an internal frontier model after consulting the Advisory Group, publishing them on GitHub with protocols for revisions and citations, still exploring community-hosted alternatives that meet the committee's guidelines, adding Lean formalisations as obtained, publishing 10.

AHM statement on OpenAI’s 6 October release

Association for Human Mathematics, Communications Working Group, 2026-10-07, Findings cited with credit. Licence: none stated.

A statement from a new association of mathematicians urging colleagues to stop working with OpenAI and the public to treat this publication model with scepticism, hosted on its own site and reposted on a mathematician's blog.

4 findings on families: 146, 148, 153

Statements - AHM

Association for Human Mathematics, 2026-10-07, Linked. Licence: n/a.

Statements page of the Association for Human Mathematics holding the 7 October statement on OpenAI's release and a selection of members' comments to the advisory group.

openai/math README and history.md at commit fd4aeeb

OpenAI, 2026-10-07, Linked. Licence: n/a.

The repository's own record: 719 manuscripts in 372 families after three withdrawals, about 42% (300 of 719) of top-line results formalised, 14 manuscripts revised and 13 re-dated, six new formalisations and five other additions on 7 October, ten reasoning summaries.

OpenAI math repository: proofs and Lean formalisations

Chris Birkbeck, 2026-10-06, Findings cited with credit. Licence: none stated.

A 24-page AI-made table, requested by a Lean mathematician and posted the evening of the release, listing every family with whether the repository links a Lean scope page and which Comparator files cover it; its headline is 235 of 372 families formalised.

Lech’s conjecture in equal characteristic: exposition of a proof found with ChatGPT Astra

Srikanth B. Iyengar, Linquan Ma, Mark Walker, Alex Gerko, 2026-10-06, Linked. Licence: none stated.

A preliminary exposition by Iyengar, Ma and Walker of a proof of Lech's conjecture in equal characteristic that Alex Gerko found with ChatGPT Astra, posted with the original AI-written manuscript and two AI-generated retrospectives; the page says it was first posted on 5 October.

1 finding on family: 194

Navier-Stokes lost in translation

Alexander Bastounis, Fabian Circelli, Anders C. Hansen, 2026-10-06, Findings cited with credit. Licence: none stated.

An arXiv paper arguing that a Lean check of an AI formalisation does not guarantee that the natural-language proof is the one proved, with OpenAI's Navier-Stokes blow-up announcement as the lead example; it concerns that earlier claim, not a family of this collection.

Ten advances in mathematics and theoretical computer science

OpenAI, 2026-08-01, Linked. Licence: n/a.

Earlier OpenAI release of ten results (sphere packing, binary and spherical codes, non-sofic groups, Connes rigidity, permanent lower bounds, quantum parallel repetition, closest vector problem, Ehrhart's volume conjecture, multicolour Ramsey, extremal number conjectures) from an internal Astra model, with Lean certificates.

Announcing FrontierMath Erdős

Tom Adamczewski, Greg Burnham, 2026-09-01, Linked. Licence: n/a.

Epoch's benchmark of 68 Erdős problems open as of August 2026, selected by Thomas Bloom, scored by whether a model produces a Lean proof or disproof that passes the Lean FRO's Comparator.

Covers family: 167

Navier-Stokes as a worked example of AI solutions contaminating a field

Terence Tao, 2026-09-03, Linked. Licence: n/a.

Framing piece five weeks before the release. Tao describes a scenario in which an autonomous AI harness settles the Navier-Stokes regularity problem while keeping the iteration that found the ansatz out of public view, so the problem is solved but the field gains little. On 5 Sep they added that they knew of no solution yet.

2 findings on family: 376

To grieve, or not to grieve?

Kevin Buzzard, 2026-10-01, Linked. Licence: n/a.

Written five days before the release. Buzzard sorts mathematicians' reactions to AI by Kubler-Ross stages, then argues they are excited and that the community should demand OpenAI simply dump its collection of results so humans can see what is claimed, with tidying later. They signed the 'Release the Proofs' open letter.

Changes to the Erdos problems web site

Thomas Bloom, 2026-10-06, Linked. Licence: n/a.

Bloom's guest post, crossposted from the Erdos problems forum, on how AI solutions with no explanation have displaced and discouraged human work on the problems and how the site will change in response; published the day of the release.

Covers family: 159

Post listing quantum information results in the release

Isaac Kim, 2026-10-06, Linked. Licence: n/a.

A quantum information researcher calls the quantum-information, many-body physics and quantum-computing content of the release shocking and singles out the 2D area law, the spin-one Haldane gap, parity not in QAC0, a constant-error version of the Aaronson-Kuperberg conjecture and unitary vertex operator algebras generating.

3 findings on families: 265, 268, 274, 280, 283

Post on the matrix multiplication exponent 2.25

Steven Strogatz, 2026-10-06, Linked. Licence: n/a.

Strogatz calls many results staggering and picks the matrix multiplication exponent bound of 2.25, which beats a previous record near 2.37, comparing the jump to Bob Beamon's long jump.

Covers family: 107

Post praising the quasi-Riemann and no-Siegel-zero results

Levent Alpoge, 2026-10-06, Linked. Licence: n/a.

A mathematician who describes themselves as having talked about this being within reach gives big credit for the quasi-Riemann and no-Siegel-zero results and mentions sad stories of users being scooped or in conflict with the labs.

1 finding on family: 003

Post reacting to the quasi-Riemann hypothesis result

Alex Kontorovich, 2026-10-06, Linked. Licence: n/a.

Within an hour of the release Kontorovich says that a human proving the quasi-Riemann hypothesis would get an instant Fields Medal, and explains that the best previous result was a zero-free region that thinned with height, whereas the new result gives a fixed strip.

Covers family: 003

Slopocalypse

Peter Woit, 2026-10-06, Linked. Licence: n/a.

Blog post calling the release a disorganised 'slopocalypse', criticising OpenAI for ignoring the advisory group's recommendations and the group's own statement, and arguing the aim was to carpet-bomb a research incentive structure.

2 findings on families: 311, 376

The OpenAI problem dump

Frank Calegari, 2026-10-06, Linked. Licence: n/a.

Posted the morning of release day as an 'exam' of open problems in algebraic number theory (Lehmer, Artin, modularity over number fields, Leopoldt, BSD, Vandiver and others), written before the repository appeared.

2 findings on families: 003, 029, 030

Thread on 'Math 1.0' and 'Math 2.0' (posts 1/4 to 4/4)

Terence Tao, 2026-10-06, Linked. Licence: n/a.

Posted at 18:00 UTC on release day. Tao contrasts a traditional breakthrough, which generates talks, workshops, collaborations and digestion, with AI-prompter solutions whose authors cannot answer questions. They argue that solved problems cannot be un-solved and that harvesting them at scale leaves fields less fertile.

Open No More

Lance Fortnow, 2026-10-07, Linked. Licence: n/a.

Fortnow inserts a note at the top of a previously written post: the release contains theory-of-computing results (Unique Games, L = BPL, matrix multiplication at n^(2.25+epsilon), several flagged as Lean-formalised), which if they hold would be more progress in 24 hours than in the previous three decades.

2 findings on families: 102, 103, 107

Post on the 9/4 matrix multiplication paper and its all-fields extension

Thomas Dybdahl Ahle, 2026-10-07, Linked. Licence: n/a.

Ahle reports that someone generalised the OpenAI n^2.25 matrix multiplication algorithm to all fields and that it seems to check out in Lean, and calls the new paper surprisingly elegant: instead of powering and trimming the Coppersmith-Winograd tensor it defines a potential function on tensors and argues by contradiction.

Covers family: 107

Posts on the plane-colouring (chromatic number at least 6) proof

Dmitry Rybin, 2026-10-07, Linked. Licence: n/a.

Rybin says they found the OpenAI proof that the chromatic number of the plane is at least 6 unbelievably alien: it shows any K-colouring is equivalent to a 'weakly measurable' K-colouring, which seems out of nowhere, and then uses heavy human-developed machinery (amenable groups, Pontryagin duality, Furstenberg-Zimmer towers).

2 findings on family: 158

Classical at Heart (Substack)

Dakshita Khurana, 2026-10-08, Linked. Licence: n/a.

A researcher who spent three years on unitary synthesis describes believing the unpopular positive answer, recognising familiar ideas in OpenAI's manuscript (recursive implementation through a smaller unitary, sparse-row almost-isometries), and what the result would mean for quantum cryptography if it holds.

Covers family: 283

Post publishing a tightening of OpenAI problem 109 (integer multiplication)

Doug Colkitt, 2026-10-08, Linked. Licence: n/a.

Colkitt announces an update to the integer multiplication result: the saving constant kappa goes from 2 to the minus 182 to 2 to the minus 34, a roughly 48 million-fold improvement over the previous community figure, by moving compact control bits instead of whole windows.

Covers family: 109

Tweet reporting a flaw in the Weil classes manuscript

Elliot Glazer, 2026-10-08, Linked. Licence: n/a.

The earliest public report we found that the manuscript on Weil classes on split abelian eightfolds is flawed, posted about two and a half hours before OpenAI announced its withdrawal.

1 finding on family: 032

Working notes on the quasi-Riemann hypothesis papers

Michael Rubinstein, 2026-10-09, Linked. Licence: n/a.

A number theorist's reading aids for OpenAI's quasi-Riemann papers, generated with Claude and Codex and explicitly unchecked in detail: accessible 16-page and 12-page guides to the 11/12 and 7/8 arguments for zeta, a 29-page adaptation of both methods to the L-functions of the CM curves y^2 = x^3 + d (its 7/8 part is an outline.

2 findings on family: 003

OpenAI Releases 722 Math Manuscripts From an Unreleased AI Model

Unite.AI, 2026-10-06, Linked. Licence: n/a.

Detailed paraphrase of OpenAI's post and README: 722 manuscripts in 372 families, about 4,000 problems, three hours average compute, two named exceptions, the ten reasoning-summary topics and a long account of the advisory group's 29 September recommendations (over 600 replies from the community).

Covers families: 003, 017, 087, 197, 221, 287, 362

OpenAI drops another batch of mathematical breakthroughs

Robert Hart, 2026-10-06, Linked. Licence: n/a.

Short same-day report quoting OpenAI's description of the release and the advisory group's September recommendations (release promptly, disclose model, prompts and compute, avoid using results as marketing); also records OpenAI's September claim of more than 100 resolved open problems.

OpenAI unleashes hundreds more math results upon a field already in shock

Joseph Howlett, 2026-10-06, Linked. Licence: n/a.

Same-day report that OpenAI published 372 results in a GitHub repository; an OpenAI spokesperson said almost every result came from one prompt to one agent, some needed several attempts, many results are not yet understood by OpenAI's own mathematicians, and OpenAI is not bound by the advisory group's recommendations.

As AI Closed In on 'Unique Games' Proof, Researchers Raced to Beat the Machines

Ben Brubaker, 2026-10-07, Linked. Licence: n/a.

Tells how Dor Minzer, Yumou Fei and Shuo Wang rushed out a 95-page human-written result on a variant of Khot's 2-to-1 games conjecture when rumours spread that OpenAI had proved the unique games conjecture, then reports that OpenAI's 6 October release did contain such a proof.

1 finding on families: 102, 106

OpenAI Dumps 377 New Math Results on GitHub, Publishes Hand-Wringing Blog Post

Mike Pearl, 2026-10-07, Linked. Licence: n/a.

Snarky news item: 377 new results, one paper claiming the full Birch-Swinnerton-Dyer leading-term formula only for elliptic curves over Q with low Selmer corank, and a note that the advisory group's request to stop testing proprietary models was not taken up.

Covers family: 002

OpenAI Releases AI-Generated Proofs Of Quasi Riemann Hypothesis, Unique Games Conjecture & Hodge Conjecture For CM Abelian Varieties

OfficeChai Team, 2026-10-07, Linked. Licence: n/a.

Explains the four results Sam Altman singled out as the biggest: the quasi-Riemann hypothesis, the Unique Games Conjecture, the rational Hodge conjecture for CM abelian varieties and the free group factors problem, noting that the first, second and fourth have Lean proofs and the Hodge one did not yet.

2 findings on families: 003, 032, 102, 287

OpenAI Releases Over 300 Mathematical Results Produced By An Internal Model

OfficeChai Team, 2026-10-07, Linked. Licence: n/a.

Walk-through of the README: 722 manuscripts in 372 families across 16 areas, a table of families per discipline, the fixed production procedure with two exceptions (the zeta zero-free region and the Hodge conjecture for CM abelian varieties), and the open questions about verification.

Covers families: 003, 032

OpenAI publishes 722 maths papers written by a model it has not released

Ana Maria Constantin, 2026-10-07, Linked. Licence: n/a.

Summarises the README and OpenAI's post: 722 manuscripts in 372 families, about 4,000 problems, three hours of compute, ten summaries and two results that did not follow the standard procedure (a zeta zero-free region and the Hodge conjecture for CM abelian varieties).

Covers families: 003, 032

OpenAI mistranslated mathematics into code for its Navier-Stokes proof

Jacob Aron, 2026-10-08, Linked. Licence: n/a.

Reports a Cambridge and King's College London team's finding that OpenAI's Lean version of its September Navier-Stokes proof does not match the natural-language PDF at Lemma 8.6 (a bound of m+4 versus m+5), and what that implies for the 722 papers just released, only some of which have Lean proofs.

Covers family: 376

OpenAI’s math solutions aren’t meeting the field’s standards yet

Tim Fernholz, 2026-10-08, Linked. Licence: n/a.

Argues that OpenAI fell short of its advisory group's standards: it keeps testing proprietary models, gave chain-of-thought for only 10 of 719 manuscripts, and did not add machine-readable links between natural-language and formal proofs.

The most exciting claims from OpenAI’s heap of new proofs

Scientific American (byline not recorded), 2026-10-08, Linked. Licence: n/a.

Walks through the headline claims by field with named specialists commenting: quasi-Riemann hypothesis and Siegel zeros, Hilbert's tenth problem over the rationals, four-dimensional Kakeya, a sigma-model analogue of Yang-Mills, matrix multiplication at 9/4, L = RL = BPL, the Unique Games Conjecture, unitary synthesis.

10 findings on families: 003, 004, 074, 102, 103, 107, 109, 130, 215, 267 …

'Pure insanity': Mathematicians will need years to make sense of OpenAI’s latest drop

Robert Hart, 2026-10-09, Linked. Licence: n/a.

Survey of more than three dozen mathematicians: awe mixed with anxiety, difficulty reading the papers, uneven formalisation, concerns about thin attribution and short bibliographies, reports of research programmes made redundant, and a view that OpenAI followed some but not all of AGMAI's recommendations.

2 findings on families: 003, 032, 074

New Math from OpenAI

Zvi Mowshowitz, 2026-10-09, Linked. Licence: n/a.

Long commentary post on the release: 722 manuscripts (719 after three withdrawals) in 372 families from about 4,000 problems, 90 of the top 500 open problems according to ProofAtlas, Lean coverage of five of nine headline results, and a survey of reactions including Aaronson, Tao's Math 2.0 and the AHM statement.

4 findings on families: 002, 003, 004, 017, 032, 102, 107, 109, 157

Quanta: Cracks appear in OpenAI’s wall of proofs (and the 6 October piece)

Konstantin Kakaes, 2026-10-09, Findings cited with credit. Licence: none stated.

Quanta's running coverage records experts saying some papers are too vague to check, that a three-dimensional tile paper has new ideas but is hard to read, that some Lean statements may prove less than the papers, and that proofs should be treated as raw data.

1 finding on family: 155

openai-zeta-proof-check

davegoldblatt, 2026-10-07, Findings cited with credit. Licence: MIT.

An independent re-run, carried out by an AI agent at the author's request, of the Lean check for the quasi-Riemann zeta bound with Comparator and a second kernel, with logs and a container recipe.

2 findings on family: 003

pts-normalization: a confined copy of the OpenAI strong normalisation proof

Talia Ringer, Jamie (student, surname not shown), 2026-10-07, Linked. Licence: none stated.

A trimmed copy of the repository holding only the pure type systems normalisation proof, on which a student ran Comparator with the second kernel enabled and reports acceptance, with the caveat that an AI model extracted the files.

1 finding on family: 245

FineEnvs/openai-math

FineEnvs, 2026-10-08, Linked. Licence: apache-2.0.

A Hugging Face dataset of 369 reinforcement-learning environments built from the Lean challenges whose official proofs were verified end to end in a sandbox, out of 405.

Lean Zulip: OpenAI releases solutions to hundreds of problems

Joseph Myers, Jack McCarthy, David Michael Roberts, Chris Henson, Kevin Buzzard, David Ang, Johan Commelin, Alex Meiburg, 2026-10-06, Linked. Licence: n/a.

The main Lean community discussion of the release, opened within an hour of the announcement, where members asked for a paper-to-Lean map, reviewed statements, found and repaired the Comparator definition holes, and argued about norms for releases of formal proofs.

100+ reactions to 100+ solutions (Proofs and Prompts)

Hosts of Proofs and Prompts, 2026-10-08, Findings cited with credit. Licence: none stated.

A communal blog post gathering roughly one hundred signed reactions from mathematicians to the release, covering awe, grief, anger at unreadable papers, calls for neutral reading groups and a platform for discussion, and new norms for credit.

7 findings on families: 214, 250, 252, 254, 290

Comments on 'Erdős problems in the OpenAI proofs'

MalekZ, jleng01, NicoV, efiebig, Thomas Bloom, 2026-10-08, Findings cited with credit. Licence: none stated.

Nine comments on the maintainer's list, which record a reading experience of the longest manuscript, an opinion that its length is useful mainly to another AI, consequences for a Ramsey problem and two earlier claims of the same decomposition result.

3 findings on families: 159, 170, 181

MathOverflow: how can one contact the authors regarding corrections or missing references?

Jialong Deng, Sam Hopkins, Emil Jerabek, David White, Timothy Chow, Dimitri Vulis, TimH, 2026-10-08, Findings cited with credit. Licence: CC BY-SA (Stack Exchange network default).

A question from a mathematician who says two families generalise their results without citing them and who could not find any address for the authors; the comments ask for human authors and a correspondence address, and an answer proposes venues and a fork that accepts issues.

2 findings on families: 335, 336

MathOverflow: how many of the released results went against the conventional wisdom?

tparker, Philip Weiss, Will Sawin, Nik Weaver, Pace Nielsen, mathworker21, Joshua P. Swanson, Timothy Chow, Daniel Soltesz, 2026-10-08, Findings cited with credit. Licence: CC BY-SA (Stack Exchange network default).

A community-wiki style question whose answers name which released results contradicted expert expectations, with experts commenting field by field and a close vote that was reversed.

11 findings on families: 003, 076, 109, 131, 132, 168, 169, 205, 283, 297

Top Open Problems in Math by LLM-Assessed Importance

zone411, 2026-10-06, Linked. Licence: none stated.

An LLM-ranked list of 500 open problems whose maintainer counted, in the main Hacker News thread, how many the release addresses; readers asked for a disclosure of how the ranking was made.

Abhishek Saha four-category scheme

Abhishek Saha, 2026-10-07, Findings cited with credit. Licence: none stated.

A professor's four-category rubric from non-breakthrough to shock breakthrough applied loosely to the release, naming the quasi-Riemann result as the single shock.

Covers family: 003

wardalxndr/openai-math-explorer: question answering with page citations

wardalxndr, 2026-10-07, Linked. Licence: none stated.

A small retrieval-augmented question-answering app over the release overview, the ten reasoning traces and family metadata that cites file and page for every answer, shows a Lean-status badge and carries a 30-question retrieval test set.

own-your-specs

Yannick Forster, 2026-10-09, Linked. Licence: none stated.

A minimal example showing how a definition listed as overridable lets a Comparator check pass for a changed statement, with a proposal to rename the field so the risk is obvious.

1 finding on family: 158

ProofSearch errata: a public report tracker for the release

Paras Koundal, 2026-10-07, Linked. Licence: none stated.

An issue tracker with one report per manuscript in seven types (suspected error, gap in a proof, Lean statement differs from paper, citation, typo, independent check with no problem found, question) and maintainer labels acknowledged, fixed and disputed; no reports filed by 11 October.

Erdős problems in the OpenAI proofs

Thomas Bloom, 2026-10-08, Findings cited with credit. Licence: none stated.

The Erdős problems site maintainer's list of 25 problems with claims in the release, giving for each the problem, the OpenAI PDF, the Lean challenge or its absence, earlier work they name and a short remark, with a disclaimer that they have checked neither the proofs nor the Lean statements.

24 findings on families: 011, 012, 013, 021, 024, 025, 026, 028, 076, 084 …

Paureel/beyond-n-log-n

Aurel Prosz, 2026-10-08, Linked. Licence: apache-2.0.

A live tracker page for the community race on the integer multiplication exponent.

Covers family: 109

zjukop3/openai-math-tracker

zjukop3, 2026-10-08, Linked. Licence: Apache-2.0 per README (GitHub shows no licence file).

A bilingual machine-readable catalogue of the manuscripts with a pull-request based verification tracker.

Atlas survey of Erdős problem pages, recorded on 11 October 2026

Compiler not recorded (Atlas survey), 2026-10-11, Linked. Licence: n/a.

An imported Atlas survey of 25 problem pages linked from Thomas Bloom’s OpenAI post. The survey compiler is not recorded. Bloom and the erdosproblems.com contributors authored the underlying pages; this survey is not a post or review by Bloom.

3 findings on families: 024, 167, 170, 181