What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics

Ying Xie

math.HOOct 12, 2026

What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics

Authors: Ying Xie

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

Table 1: Summary figures of the extraction (as of 11 Oct 2026).

Family	Result	Lean	Central extracted instrument	Verdict
003	$\zeta$ and Dirichlet L zero-free for $\operatorname{Re}s>7/8$	partial inspection	Twist the Möbius sum by all sextic residue symbols; Poisson fuses $\mu$ 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 $\mathbb{Q}$ undecidable	no	The reduction does not construct a Diophantine definition of $\mathbb{Z}$ . 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 $\pi$ 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 $\mathbb{R}^{3}$ ; Kakeya sets in $\mathbb{R}^{4}$ 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 $k\to\infty$ ; the volume product becomes a sum of feasibility probabilities over signed simplices packing inside the polar.	new feasible-simplex identity; rest combination

Table 2: The map, first group: 17 families.

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 $\mathrm{AC}^{0}$ .	combination bordering new
010	Fontaine–Mazur modularity at $p=2$ , 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 $p_{g}=0$	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	$\mathrm{L}=\mathrm{RL}=\mathrm{BPL}$	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 $2^{\omega(\sqrt{n})}$	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 $pk$ ; the standard switching bound $(5pk)^{s}$ gives decay in $s$ when $pk<1/5$ .	new

Table 3: The map, second group: 21 families.

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	—

Table 4: Verification and dependency scoreboard (initial extraction labels with selected source corrections).

AI-Assisted Mathematical Discovery

See all 18 papers

Aug 3, 2026

A Human Audit of OpenAIs AI-Generated Mathematical Proofs

We assess 18 chapter-specific reviews of the ten mathematical results announced by OpenAI on 1 August 2026, alongside review standards, Lean formalizations, subsequent research, and mathematical references. The article audits this review record without claiming a complete reconstruction of all ten proofs. No confirmed substantive mathematical error in a principal result remains in the examined assessments, although review depth varies and some dependencies remain partly checked. Chapter 8 presents the strongest reservation: a specialist review requests major revision of compressed analytic arguments. In Chapter 6, an apparent polarity error was withdrawn after an overbar lost during PDF extraction was recovered from the typeset source. Subsequent research independently reuses the Chapter 3 proof mechanism and confirms that Connes's rigidity conjecture is false, without independently reproducing Chapter 4's stronger infinite-family result. Among the cited follow-ups, Chapter 7 receives the strongest direct theorem-level corroboration through a stronger hardness theorem. Related equality results in Chapter 8 do not verify the analytic inequality proof. Some follow-ups disclose material AI assistance. We argue that confidence should combine formal checking, human reconstruction, independent mathematical use, and a public record supporting correction of both proofs and reviews.

Mikołaj Sienicki, Krzysztof Sienicki

Polish-Japanese Academy of Information Technology ul. Koszykowa 86, 02-008 Warsaw, Poland, European Union · Chair of Theoretical Physics of Naturally Intelligent Systems (NIS)1 ul. Lipowa 2 / Topolowa 19, 05-807 Podkowa Leśna, Poland, European Union

LLM Auditing Human Oversight of AI LLM Mathematical Reasoning Reasoning Verification

Ask PDF

May 27, 2026

ResearchMath-14K: Scaling Research-Level Mathematics via Agents

The frontier of mathematics is defined by problems whose solutions are not yet known. However, whether language models can meaningfully engage with such problems without human intervention remains unclear. A major obstacle is the lack of large-scale research-level math datasets. To this end, we introduce ResearchMath-14k, a set of

14{,}056

problems curated from academic sources via a multi-agent pipeline. ResearchMath-14k spans 11 mathematical domains and ranks above existing math datasets on knowledge, novelty, and procedural difficulty. To our knowledge, it is the largest research-level mathematical problem set available for training. We additionally generate

220

K teacher trajectories through targeted prompting, followed by behavioral filtering. Notably, however, generating correct trajectories is nontrivial at this level, and two LLM judges label only

3.7\%

and

4.3\%

of sampled ResearchMath training trajectories as correct. Nevertheless, across three model families, full-parameter training on ResearchMath improves performance on graduate- and research-level mathematics benchmarks by

2.1

points over the starting checkpoints. In comparison, training on existing datasets such as DASD and Nemotron-SFT-Math-v4 changes performance by

0.0

and

-0.5

points, respectively. Notably, mixing DASD with ResearchMath yields higher scores than token-matched DASD alone on benchmarks covering olympiad short-form (

+2.0

), graduate- and research-level short-form (

+0.8

), graduate- and research-level symbolic (

+2.6

), and proof evaluation (

+5.7

). Further analysis suggests that research-level mathematical content and greater reasoning diversity may help explain why ResearchMath provides complementary supervision to contemporary datasets. We make ResearchMath-14k publicly available for future works on research-level mathematical reasoning.

Guijin Son, Seungyeop Yi, Minju Gwak +3

Seoul National University · OneLineAI · Yonsei University

Supervised Fine-Tuning LLM Mathematical Reasoning

Ask PDF

Jul 10, 2026

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems

Large language models (LLMs) have shown increasing promise in solving open problems in mathematics. However, their performance can be further improved through agentic workflows tailored to real-world mathematical practice. To this end, we introduce ProofCouncil, a mathematical agent that is designed to tackle open problems using an author-critic architecture. ProofCouncil served as a submission to the second batch of FirstProof, a challenge consisting of 10 real-world mathematical problems that agents must solve autonomously. Its submissions for 6 of the 10 problems were judged by the referees to be correct up to at most minor revisions, showing the best performance among participating teams. We also evaluate ProofCouncil on 30 open problems collected from mathematical researchers. Among the 21 solutions that received human feedback, 5 were judged completely correct, 2 more were judged promising pending final verification, and a further 8 contained useful partial progress. In this short paper, we describe the development of ProofCouncil and the agent-building library used to create it, which we release as open source to the community.

Johannes Schmitt, Tim Gehrunger, Jasper Dekoninck +4

ETH Zurich · Aarhus University · Independent Researcher +1

LLM Agents Multi-Agent LLMs LLM Mathematical Reasoning

Ask PDF

Abstract

AI-Assisted Mathematical Discovery

Explore similar work

A Human Audit of OpenAIs AI-Generated Mathematical Proofs

ResearchMath-14K: Scaling Research-Level Mathematics via Agents

ProofCouncil: An LLM Agent for Solving Open Mathematical Problems