What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics
Organizations: Kennesaw State University
Abstract
On 6 October 2026 OpenAI published an initial 722 AI-written mathematical manuscripts, organized into 372 problem families, in the public repository github.com/openai/math. The release includes claimed solutions to many prominent open problems. We approach this collection as a treasure mine of mathematical ideas. Our aim is to extract new lemmas, constructions, inequalities and proof mechanisms introduced in the source arguments, and to distinguish them from established tools and new combinations of those tools. We call these mathematical instruments. Extraction comes first; their validity, novelty and possible reuse then become subjects for further study. The resulting descriptions also help readers understand the selected papers without having to reconstruct every argument at the outset. We examine 38 families in two groups of 17 and 21, spanning number theory, geometry, analysis, combinatorics, complexity, algebra, operator algebras, topology and mathematical physics. Each entry records the claim, extracted instruments, antecedents and caveats. Eleven cross-cutting patterns connect the entries, and a scoreboard records formalization status and dependencies. Novelty assessments are provisional and sometimes mixed. Selected source comparisons correct mathematical statements, hypotheses and counts; they do not independently establish priority or certify the underlying proofs. No Lean development was compiled or kernel-checked for this survey. We also briefly describe a subsequent application of the signed restriction lemma from family 112 to circuit lower bounds at every fixed depth.
Figures & tables
| Quantity | Value | Note |
|---|---|---|
| Families examined | 38 | selected for the prominence of the problem, across number theory, geometry, analysis, combinatorics, complexity, algebra, operator algebras, topology and mathematical physics. Group 1: 17 families. Group 2: 21 families |
| Novelty classifications | qualitative | Mixed labels are retained at the family and instrument level. No disjoint numerical breakdown is asserted, and novelty judgments have not been independently validated by the subsequent mathematical review |
| Original headline-formalization labels | 19 of 38 | Includes partial inspection for 003 and 087. Five other original entries were companion-only, counting 159. These are labels from the initial extraction; source-status corrections and the counting rule appear in Section 10 . No Lean build was run |
| Recurring pattern | Established methods in new settings | a 1983 theorem on maps without approximate fixed points is applied to amenability; a 2009 circuit-complexity theorem to Chowla correlations; Quot-scheme localization to Bloch; a 2019 conformal map to Mahler |
| Family | Result | Lean | Central extracted instrument | Verdict |
|---|---|---|---|---|
| 003 | and Dirichlet L zero-free for | partial inspection | Twist the Möbius sum by all sextic residue symbols; Poisson fuses with Gauss sums into cubic Gauss sums, whose Kubota–Patterson automorphy moves the thin sextic family to a quadratic one where square-root cancellation on average is known. | combination as architecture, leaning new |
| 004 | Hilbert’s tenth problem over undecidable | no | The reduction does not construct a Diophantine definition of . A Turing reduction dovetails integer-root enumeration with finite rational-oracle tests. Compactness and elliptic height bounds show that some finite test fails if no integer root exists. Every terminating run makes finitely many queries, with no uniform bound asserted. | new |
| 017 | Irrationality exponent of equals 2 | yes | “Separated-weight interpolation”: jets at translates on the exponential curve with anisotropic weights chosen independently of the centers, while the sufficiently large degree threshold may depend on them, proved by a Dyson-type curve inequality pushed through nef/ample and Serre vanishing on a weighted blow-up. | combination bordering new |
| 032 | Rational Hodge conjecture for CM abelian varieties | no | “Fixed-input variation”: freeze the theta-series input on a Picard-type ball quotient, move only the definite-place complex structure, keep a (2,0)-form period nonzero, then rationalize by weak approximation. | combination |
| 074 | Kakeya maximal conjecture in ; Kakeya sets in have dimension 4 | no | Differentiate the critical exponent: BV gives approximate differentiability of the exponent surface; a separate monotonicity argument yields an ordinary differentiability point whose partial derivatives prescribe extremal configurations ruled out by an entropy and mutual-information bound. In 4D, a variational “horizon” built from quadratic local fits replaces polynomial Wolff axioms. | combination leaning new; 4D framework new |
| 087 | Mahler conjecture, symmetric and general | symmetric | Replace each real strip by a complex lens with uniform boundary coordinate (Gross’s conformal Skorokhod map); push Lelong-number Jacobian mass to the boundary as ; the volume product becomes a sum of feasibility probabilities over signed simplices packing inside the polar. | new feasible-simplex identity; rest combination |
| Family | Result | Lean | Central extracted instrument | Verdict |
|---|---|---|---|---|
| 002 | Full BSD formula in Selmer corank 0 and 1 | no | “Tame variables”: ultrafilter limits of cyclic characters at auxiliary primes used as extra Iwasawa variables to force integrality with no residual-image hypothesis; a “theta implication” comparing Artin lengths from a holomorphic theta family on U(3,1) with a nilpotent parameter replaces Eisenstein congruences. | new construction; rest combination |
| 007 | Ordinary two-point Chowla; corrected binary Elliott | original: statements only; see card | “Terminal-scale divisor bins”: dilations confined so narrowly that the scale is unchanged, removing Tao’s logarithmic averaging; integers certified to behave like independent residues by Braverman’s theorem that polylog independence fools . | combination bordering new |
| 010 | Fontaine–Mazur modularity at , all residual types | no | “Marked lines”: after a huge abelian 2-extension, record an ordinary line at only a vanishing fraction of dyadic places, enough to force the residual fiber connected while leaving the propagation step unrestricted at 2. | combination |
| 040 | Bloch’s conjecture for all surfaces with | no | Apply virtual enumerative geometry to a Chow problem: a torus-localized Quot-scheme count with two copies of the surface left unintegrated vanishes for degree reasons, so fixed loci give a diagonal decomposition with a universal coefficient; for fake projective planes the coefficient is read on a Cartwright–Steger surface. | new strategy |
| 103 | yes | “Exact correction and copy hierarchy”: no pseudorandom generator; refine the configuration graph algebraically so every transition weight is small, estimate the reward with a sampler driven by one O(log n)-bit environment, and control the evaluator’s recursive space use with a catalytic key-equality gadget. | new | |
| 112 | Explicit depth-3 circuit lower bound | yes | “Restriction bound independent of clause count”: a restricted width-k CNF written as a signed combination of width-b CNFs with bounded expected mass, with a suitable testing width for any fixed ; the standard switching bound gives decay in when . | new |
| Family | Lean label | Statement faithful? | Depends on other OpenAI papers? | Uncited nearest ancestor |
|---|---|---|---|---|
| 003 | zeta partly inspected; Dirichlet/Hecke declarations also located | not inspected | no (cubic first-moment paper cited, unused) | — |
| 004 | no | — | yes : FM modularity at 2; pointwise 2-converse | — |
| 017 | 867 files, not in catalogue | yes (eventual bound and sSup form) | no | Masser 1981; Fischler–Nakamaye 2014 |
| 032 | no | — | no load-bearing (family 001 in a remark only); withdrawn papers never cited | — |
| 074 | no | — | 3D: alternative route only. 4D: cites 3D for a lemma that is really GWZ 2026 | Rios–Sawyer |
| 087 | original: symmetric; general/polar modules supplied, unbuilt | symmetric statement only in initial extraction | no | — |