OpenAI Releases 722 Mathematics Manuscripts: On Which Unsolved Problems Has AI Proposed Breakthroughs?

In an official announcement, OpenAI released a collection of mathematical research results generated by an internal frontier model. The GitHub repository contains 722 manuscripts, grouped into 372 related result families spanning number theory, geometry, mathematical physics, and theoretical computer science.

These manuscripts propose concrete answers and proof approaches to long-standing unsolved problems. Examples include establishing that the irrationality exponent of pi (π) is 2, proving that the three-dimensional relativistic plasma equations remain smooth under specified large initial data, constructing an algebraic counterexample where ab = 1 yet ba ≠ 1, and eliminating the additional conjecture underlying the hardness of approximation for Max-Cut. Respectively, they investigate: how closely fractions can approximate π, whether equations will lose control within finite time, whether a classic conjecture holds true, and how strong the guarantees of fast algorithms can be.

These conclusions are at varying stages of verification; nor do 722 manuscripts represent 722 independently solved problems. This release also provides formal Lean code for select propositions and 10 reasoning trace summaries, enabling the outside world to inspect the papers, derivations, and exploratory processes. Below, we first examine the specific mathematical advances, then see how they were generated and how far verification can proceed today.

Six Examples to Understand What These Mathematical Conclusions Address

The six examples below cover proofs of conjectures, counterexamples disproving conjectures, and theoretical limits of algorithms. Several new results were also utilized in subsequent investigations, forming chains of derivation that can be traced forward.

1. The Quasi-Riemann Hypothesis: Ruling Out a Region Still Does Not Equal Finding All Zeros (Family 003)

The Riemann Hypothesis is one of the celebrated Millennium Prize Problems, concerning the fundamental distribution of prime numbers. The hypothesis asserts that all non-trivial zeros of the Riemann zeta (ζ) function lie on the line in the complex plane where the real part equals 1/2 (where Re(s) denotes the real part of the complex number s). Because proving this line directly is extraordinarily difficult, number theory retreats to studying the weaker "Quasi-Riemann Hypothesis": whether one can prove the existence of some constant θ < 1 on the right side of the complex plane such that the half-plane Re(s) > θ contains absolutely no zeros.

In Family 003 of the repository, the main paper claims to prove that for all Dirichlet L-functions (including the Riemann ζ function) and finite-order Hecke L-functions over specific imaginary quadratic fields, there are no zeros in the half-plane Re(s) > 7/8 (allowing for the pole at s=1); another paper in the same family provides an alternative proof for Re(s) > 11/12. In terms of mathematical regions, 7/8 is closer to 1/2 than 11/12 and thus excludes a larger region of zeros; however, it does not exclude zeros in 1/2 < Re(s) ≤ 7/8, and thus does not prove that all non-trivial zeros lie on the line Re(s) = 1/2.

The family also presents a uniform exclusion result concerning Landau–Siegel real zeros (potential real zeros close to 1). In the accompanying formal Lean code, the team formalized the zero-free conclusion for Re(s) > 7/8 along with a logarithmic repulsion boundary; here, no explicit numerical value is given for the positive constant in the repulsion bound, and subsequent applications from the paper also fall outside the scope of these selected formalized statements.

2. The Approximation Limit of Pi: How Closely Can Fractions Approximate π? (Family 017)

Mathematics proved that π is irrational over a century ago; this research is neither about proving the irrationality of π nor proposing a new algorithm to compute the decimal digits of pi. Rather, it investigates the ultimate precision limit of approximating π with rational fractions. In number theory, the "irrationality exponent" characterizes this difficulty of approximation: how small the error can be when a fraction p/q with denominator q approaches a target irrational number. According to Dirichlet's approximation theorem, the approximation exponent of any irrational number is at least 2; if the exponent is exactly 2, it means that for any given ε > 0, as long as the denominator q is sufficiently large, the error cannot fall below 1/q^2+ε—that is, fractions cannot approximate the number abnormally closely at any higher order.

The significance of reaching 2 is closing the gap between the upper and lower bounds of this exponent. Dirichlet's theorem already guarantees it is no less than 2; proving that it is no greater than 2 determines the exact value rather than merely narrowing down the possible range. This is precisely the advance the manuscript claims to have accomplished.

The paper in Family 017 claims to provide a proof that the irrationality exponent of π is exactly equal to 2, and from this derives the convergence of the classic Flint–Hills series: 1/(1³ sin²1) + 1/(2³ sin²2) + 1/(3³ sin²3) + …

In this series, every term is positive; because positive integers n enter the computation in radians, whenever n happens to be extremely close to an integer multiple of π, |sin n| becomes extremely small, causing that term to explode in value. Whether this series sums to a finite result depends on whether the n³ in the denominator is sufficient to suppress these suddenly inflating terms. Limiting how closely rational numbers can approximate π helps establish an upper bound on the growth of these exceptionally large terms. However, the asymptotic lower bound provided by the irrationality exponent cannot be directly copied as a simple term-by-term bound for all positive integers n; the convergence of the series is a conclusion reached in the paper through further in-depth derivations. The accompanying Lean scope documentation covers the core proposition that "the irrationality exponent of π is equal to 2"; the convergence of the Flint–Hills series already has corollary code in Main.lean, but it is not included in the selection scope of this Comparator configuration.

3. Relativistic Plasma Systems: Can Large Initial States Evolve Smoothly Indefinitely? (Family 362)

In the field of partial differential equations, the relativistic Vlasov–Maxwell system describes the nonlinearly coupled evolution between an ensemble of charged particles and the self-consistent electromagnetic field they generate. Unlike macroscopic fluid velocity fields, this system directly models the distribution evolution of particles in phase space composed of position and momentum. Under the framework of special relativity, the velocity of an individual particle is naturally bounded by the speed of light; the core mathematical question is whether, without simplifying assumptions such as small perturbations, geometric symmetry, or electrical neutrality, assigning the system an arbitrarily large smooth initial state will cause the interaction between nonlinear fields and particle distributions to lose control in finite time, resulting in blow-up of field derivatives or loss of smoothness of the solution.

The paper in Family 362 proposes a proof of the existence and uniqueness of global classical solutions for the large-data Cauchy problem of the three-dimensional single-species relativistic Vlasov–Maxwell system. Under the established initial conditions, the initial particle density is non-negative, smooth, and compactly supported in phase space (meaning particles are confined to a bounded region of space and momentum), while the initial electromagnetic field has finite total energy, bounded spatial derivatives of all orders, and satisfies the Gauss constraints of Maxwell's equations (the compatibility condition ensuring consistency between initial electromagnetic fields and charge distributions). The paper concludes that the system maintains a smooth solution on any finite time interval and that the support of particles in phase space remains compact, thereby ruling out the formation of singularities in finite time.

Velocity has an upper bound, yet momentum can still grow arbitrarily large. In the normalized units adopted by the paper, the velocity corresponding to momentum v is u = v / √(1 + |v|²): the larger the momentum, the closer the velocity gets to the speed of light, yet it never exceeds it. Thus, the speed-of-light constraint alone cannot guarantee that solutions remain smooth. Global weak solutions for large initial data previously existed, but weak solutions do not provide the smoothness and uniqueness required here; many classical solution results relied on small data, low dimensions, or symmetry. This manuscript asserts an advance to three dimensions, for arbitrary large initial data meeting the aforementioned conditions, without requiring symmetry. Having momentum bounded on every finite time interval still permits it to grow over time.

The proof route of the original paper centers on "how to prevent momentum from becoming infinite in finite time." By first integrating directional electromagnetic forces along particle trajectories and then computing the magnitude of the net impulse, cancellations between opposing contributions are preserved; if one were to take the absolute magnitude of the force at each moment and then integrate, these cancellations would be lost. Combining directional variations of particles, residence time in dangerous angular regions, and error control, the paper establishes net impulse estimates and derives lower bounds on the time required for maximum momentum to double. The sum of these lower bounds diverges: even if each doubling occurs increasingly quickly, an infinite number of doublings cannot be squeezed into finite time. Consequently, momentum remains bounded in finite time, which, paired with continuation criteria matching initial conditions, allows the classical solution to continue evolving. This is the argumentative route proposed by the paper; the key lies in whether the new estimates hold.

This mathematical conclusion provides a formalized proposition in the Lean repository for the global existence and uniqueness of classical solutions with large initial data. This conclusion answers whether, under this equation model and specified initial data, large-scale initial states can continuously yield unique, smooth evolution; however, it is built upon an idealized single-species model and specific initial conditions, and does not equate to plasmas in real, complex physical environments never experiencing instabilities or sudden transitions under all operating conditions.

4. Specific Cases of the Hodge Conjecture: Mapping Geometric Information to Algebraic Equations (Family 032)

The Hodge Conjecture seeks to bridge two descriptions of geometric spaces: on one side lies the global geometric and topological information of the space, and on the other lie the geometric subspaces defined by algebraic equations. On smooth projective complex algebraic varieties, cohomology groups record geometric and topological information; rational cohomology classes satisfying specific complex-structure conditions are called "rational Hodge classes." The conjecture asks: can all such classes be expressed as rational linear combinations of cohomology classes of algebraic cycles? (Algebraic cycles are formed by combinations of geometric subvarieties defined by algebraic equations.) If true, these Hodge classes can be matched to geometric objects defined by polynomial equations.

The general conjecture addresses all smooth projective complex algebraic varieties. This collection of manuscripts targets specific objects: even if arbitrary dimensions and codimensions are covered on the studied objects, one must still distinguish between "holding for this entire class of objects" and "holding for all objects."

Family 032 contains 8 papers whose primary objectives focus on two specific classes of classic geometric objects: first, proving the rational Hodge conjecture in arbitrary dimensions and codimensions for all complex abelian varieties with complex multiplication (Complex Multiplication, abbreviated as CM), from which corollaries like the Tate conjecture for abelian varieties over finite fields are derived; second, proving the rational Hodge conjecture on finite products of arbitrary projective complex K3 surfaces, as well as the algebraicity of the Kuga–Satake correspondence on such surfaces. These achievements target specific classes of geometric varieties, rather than resolving the full Hodge Conjecture applicable to arbitrary smooth projective varieties.

Notably, OpenAI pointed out in the repository notes that the work on the Hodge conjecture for CM abelian varieties represents an exception outside the standard pipeline; this also indicates that the entire batch of results cannot be treated as benchmark outputs under completely identical conditions.

5. Direct Finiteness of Group Algebras: A Counterexample Where Multiplication Order Cannot Be Reversed (Family 197)

In elementary arithmetic and standard number systems, if two numbers satisfy a × b = 1, reversing their order to b × a must also equal 1. In the group algebra structures of abstract algebra, however, multiplication of elements is not necessarily commutative. The celebrated Kaplansky direct finiteness conjecture once posited: in group algebras over any field and any group, whenever ab = 1 holds, ba = 1 must follow—meaning that such algebraic systems always retain well-behaved properties akin to finite-dimensional algebras.

Family 197 delivers a negative resolution to this conjecture. The paper constructs explicit group algebra counterexamples over finite fields of characteristic two, finding algebraic elements satisfying ab = 1 yet leading to ba ≠ 1; the accompanying formal Lean code contains counterexample statements for finitely generated groups and finitely presented groups with elements of odd prime order. In mathematical research, constructing counterexamples to overturn conjectures that have persisted for decades constitutes substantive progress on par with proving theorems; this does not imply that everyday arithmetic rules for familiar numbers have changed, but rather demarcates rigorous boundaries of validity for non-commutative algebraic structures.

This counterexample was also leveraged in subsequent research. The second part of the summary takes the same pair of elements satisfying ab = 1 and ba ≠ 1 as input to construct cellular automata on infinite groups: each site takes finitely many states, new states are determined solely by finite neighborhoods, and the same rule is applied everywhere. Applying transformation b followed by a recovers the input (Ta ∘ Tb = id), so b cannot map two distinct inputs to the same output, which is injectivity; ba ≠ 1 yields an output that can never be produced by b, rendering it non-surjective. What is considered here is the infinite global configuration. The subsequent derivation relies on the aforementioned algebraic counterexample and deduces new results from it, rather than independently reproving that counterexample.

6. Max-Cut Approximation Threshold: Efficiency Limits of Deterministic Algorithms (Family 102)

The Max-Cut problem asks to partition the vertices of a graph into two sets to maximize the number of edges crossing between them. Because computing the exact optimal cut is NP-hard, algorithm design turns to rapidly finding approximate solutions. The Goemans–Williamson algorithm has an ideal approximation ratio α_GW ≈ 0.878567, or approximately 87.86%. This ratio compares the cut obtained by the algorithm against the optimal cut of the graph, not the total number of edges in the graph. The algorithm uses random hyperplanes to achieve an expected guarantee, and finite-precision implementations can come arbitrarily close to this ratio; for instance, when an optimal cut has 1,000 edges, this corresponds to an expected guarantee of nearly 879 edges, without precluding better outcomes on any particular run.

The key novelty of this work lies in changing the underlying assumption upon which the hardness result relies. The classic optimal hardness result requires the additional assumption of the Unique Games Conjecture (Unique Games Conjecture, UGC); this paper claims to eliminate it, proving that on simple unweighted graphs, achieving any fixed approximation ratio strictly greater than α_GW and at most 1 is standard NP-hard. It aims to demonstrate that this threshold limits not just a specific algorithm, but the worst-case guarantee that general approximation algorithms can offer.

The paper and its accompanying formal Lean results provide a deterministic polynomial-time reduction from binary 3SAT to the Max-Cut gap decision problem (3SAT determines whether a set of Boolean clauses can be simultaneously satisfied; it is NP-complete, with reduction time bounded by a fixed power of the input size). If a general deterministic approximation algorithm could consistently surpass the aforementioned threshold, this reduction could be used to decide 3SAT in polynomial time. Hence, under the assumption that P ≠ NP, no such algorithm exists. Removing the UGC does not prove that P ≠ NP; specific graphs may still yield better solutions, and P ≠ NP alone does not extend this impossibility conclusion to randomized algorithms.

How Did AI Generate These Research Results from Open Problems?

During model development, OpenAI evaluated models using unsolved mathematical research problems. As performance on existing mathematical benchmarks approached saturation, the team expanded these research-problem evaluations: when established problems struggle to differentiate model capabilities, harder and more open-ended questions become necessary. Portions of the new outputs were also built on top of results the model had obtained previously.

Subsequently, in their official announcement, they announced the release of this batch of findings and made the following materials public in the GitHub repository:

1. Attempts on approximately 4,000 problems: During the evaluation process, the research team presented roughly 4,000 mathematical research questions to the model. After the model produced solutions, the team aggregated them according to significance criteria, ultimately filtering and organizing them into 372 result families, totaling 722 paper manuscripts.
2. Equivalent compute consumption metric: According to OpenAI's estimates, the compute expended per result averaged approximately the equivalent computation of 3 hours of ChatGPT Pro thinking using this internal model. This is a compute estimation metric, not the actual elapsed wall-clock time or billed amount per problem, nor does it imply that the publicly available ChatGPT Pro possesses identical capabilities.
3. Reasoning traces and proof files: The release also made public 10 reasoning trace summaries from representative findings (distilled exploration and derivation logs, rather than complete raw execution transcripts), alongside formal code written in Lean for a subset of the results.

The 722 manuscripts and 372 families use different units of measurement. In this repository, a "family" represents a group of papers organized around a single core topic. It may include a main paper addressing the central conjecture, several subsidiary papers deriving corollary results, alternative proofs exploring different deductive routes, or supplementary arguments resolving technical details. Therefore, the manuscript count does not represent the number of independently solved problems; furthermore, because results were aggregated and filtered for significance, one cannot simply divide 372 or 722 by 4,000 to compute a meaningful problem-solving success rate.

The repository documentation explicitly notes that unformalized results may contain errors and pledges to correct them promptly. While most results followed the same automated pipeline, the work on the zero-free region of the ζ function and the Hodge conjecture for CM abelian varieties were exceptions; among them, the manuscript for the 11/12 zero-free region was edited by humans to improve readability.

The 372 families in the overview span 17 mathematical disciplines. Areas with the largest concentrations include theoretical computer science (40 families) and combinatorics (37 families), alongside broad coverage across algebra, number theory, differential geometry, and many other fields, illustrating the breadth of evaluation across mathematical directions.

The Value of Reasoning Trace Summaries: Revealing Self-Correction and Revision Rather Than Guarantees of Correctness

Beyond the final papers and formal code, the 10 publicly shared reasoning trace summaries offer a window into observing the model's deductive process. These summaries do not depict frictionless, straight-line proofs; instead, they reveal exploratory trajectories characterized by failed hypotheses, self-checking and corrections upon identifying contradictions, and reliance on established mathematical theorems.

For example, in the exploration record for the irrationality exponent of pi (Family 017 Summary), the model attempted a multivariable approach related to Roth's theorem; testing it against known Liouville numbers revealed the absurd implication that "the approximation exponent of all numbers is 2"—contradicting known counterexamples—which alerted the model to an overgeneralization and prompted it to recheck missing conditions. In the record for the relativistic Vlasov–Maxwell system (Family 362 Summary), the model repeatedly observed particle velocity bounds breaking down over long intervals, prompting iterative adjustments to interval-shortening factors and rigorous verification of the regularity conditions required to cite classical continuation criteria; yet the overarching argument ultimately required the model to prove the pivotal angular-occupancy and momentum estimates itself. These records capture an exploratory process containing failures, self-checking, revisions, and literature dependencies; they are condensed derivation summaries rather than independently validated certificates of correctness, and must not be used to exaggerate the completeness of all reasoning traces or the model's overall success rate.

How Far Can These Breakthroughs Be Verified Today?

Many of these manuscripts are accompanied by Lean formal proofs, offering a pathway for computers to verify logical deductions.

What Is Lean Formalization?

Traditional mathematical papers rely predominantly on natural language interwoven with mathematical formulas, frequently containing deductive steps that depend on mathematical intuition. By contrast, the interactive theorem prover Lean requires mathematical definitions, theorem statements, and every deductive step to be rigorously translated into types and code that a computerized formal system can verify item by item. When a proof script compiles completely through the logical kernel without invoking any axioms outside the permitted whitelist, one can confirm that the entire deductive chain is closed and self-consistent within the formal system.

However, the certainty of formal verification has well-defined boundaries. The machine kernel only verifies whether the given deductive steps conform to formal syntactic and type rules; it does not automatically assess whether this formalized statement remains faithful to the original paper or the core problem originally concerning the mathematical community. Still less does it evaluate whether the finding represents an original mathematical contribution, nor can it explain why the underlying mathematical ideas actually work.

Verification Logic of the Comparator Automated Judge

To evaluate batches of generated Lean proofs automatically, the community designed the judging tool Comparator. Rather than performing a surface-level, verbatim text comparison of the code, it operates within a controlled environment by exporting the syntactic environment, rigorously verifying whether the submitted Solution accurately proves the exact mathematical proposition specified by the Challenge file.

For this automated adjudication to be genuinely trustworthy, it relies on several core prerequisites: the challenge files and their dependent environment must be fully controlled and trusted, unpolluted by untrusted external files prior to compilation, the execution sandbox must function properly, and at least one underlying logical kernel must be entirely correct.

Specific Risks of "Definition Holes" and Manual Review

In formal benchmarking, there exists a specific scenario known as "definition holes". This does not mean that all formal proofs leave room for cheating, but specifically refers to certain challenges that permit solvers to fill in definitions themselves.

For example, in certain problems that require determining the truth value of a conjecture, if the challenge itself contains an uninstantiated propositional variable, the submitter might define that variable directly in the solution as "the original conjecture itself," thereby effortlessly passing machine compilation via logical reflexivity alone. Such an approach effectively bypasses the testing intent of establishing a genuine truth value. Consequently, Comparator technical documentation explicitly mandates that any challenge containing definition holes must undergo human review or additional checks to confirm whether the definition satisfies the original task intent. This is a targeted verification requirement for such challenges.

How Can These Results Enter the Mathematical Community's Shared Research?

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI) at the Institute for Advanced Study in Princeton released a public set of recommended release guidelines after receiving more than 600 submissions from the mathematical community. OpenAI consulted the group and referenced its recommendations; the advisory group articulated its own critical stance in the guidelines.

After Obtaining Answers, Humans Must Still Be Able to Explain the Proofs

The advisory group opposes evaluating advanced mathematical questions on proprietary models inaccessible to the scientific community, and calls on laboratories to cease this practice. Simultaneously, it provides recommendations for releasing results within this reality. Mathematical research seeks not only answers, but also ideas that humans can explain, and that others can understand and build upon. Traditional academic norms dictate that authors must genuinely understand every step of a proof themselves, assume full personal responsibility for correctness, and present publicly before peers at seminars to answer questions.

Accordingly, the advisory group demarcates two distinct handling pathways based on the level of human understanding of the arguments: for results where mathematicians already thoroughly understand the technical details and are willing to take full responsibility for the content, traditional scientific community norms should apply—with relevant mathematicians releasing preprints, submitting to peer-reviewed journals, and presenting at academic seminars and conferences; only when mathematical arguments produced by AI have not yet been adequately understood by the researchers who prompted them, and no human can immediately take responsibility, do the specially formulated release guidelines and accompanying funding recommendations apply. For undigested outputs, making documents public is merely the starting point; supporting mathematicians in understanding and continuing research is essential.

What Work Is Required to Integrate Results into Shared Research?

For AI mathematical outputs that no human yet fully understands, the advisory group outlined the following recommendations:

1. Supply literature attribution and improve readability: AI laboratories should search relevant literature and add citations to pertinent historical precursors; they must rewrite model outputs laden with strange jargon and verbose drafting into accessible papers that the traditional mathematical community can read, clearly presenting the problems, theorems, and proofs.
2. Preserve citable, traceable versions: Results must be deposited promptly into public academic repositories independent of commercial firms (equipped with persistent identifiers, revision histories, and preferably open peer commentary); the advisory group strongly urges avoiding the presentation of mathematical results as model marketing.
3. Disclose attempt statistics and experimental details: Laboratories should disclose model names, prompts used, chain-of-thought summaries, and compute consumption, and should also clarify how many problems of comparable difficulty failed, as well as precisely how problems were curated.
4. Formalize whenever possible: Strive to provide standardized Lean code and judge comparison artifacts, clearly stating what remains unformalized and what standard results are assumed.
5. Fund human understanding, with support allocated by independent bodies: AI companies bear a responsibility to fund dedicated workshops, working groups, postdoctoral positions, and monograph grants to assist humans in understanding this knowledge; distribution of support should be entrusted to independent non-profit entities, with comprehension efforts driven by the academic community—and accepting funds does not imply endorsement of laboratory practices.
6. Ensure equitable global access to research tools: Proprietary models risk driving a wedge between laboratories and academia, while disparate economic conditions threaten to widen access gaps. The advisory group strongly recommends providing equitable and widespread access to model capabilities across the global mathematical community, enabling broad verification, mutual understanding, and subsequent research.

What Kind of Research Material Is AI Providing for Open Mathematical Problems?

These six examples illustrate diverse avenues of mathematical advancement: discovering proofs for conjectures, disproving conjectures with counterexamples, determining worst-case capability thresholds for algorithms, and applying established results to new problems. Having saturated existing mathematical benchmarks, the team turned to unresolved research problems; this collection of manuscripts offers a concrete view of how AI participates in open-ended exploration lacking pre-existing ground truth.

OpenAI's centralized release of 722 paper manuscripts, formal Lean code for select propositions, 10 representative reasoning summaries, screening statistics across roughly 4,000 problems, and versioning mechanisms preserving revision history provides concrete case studies for observing this transition, while preparing raw source material for item-by-item verification and targeted inspection by the mathematical community.

Transforming results into reusable knowledge requires understanding why constructions work, what conditions they depend upon, and which conceptual ideas stem from existing literature. Example 5 offers a concrete demonstration: only by understanding how ab = 1 ensures inputs are not conflated and how ba ≠ 1 generates an unreachable output does one grasp how to port the algebraic construction to cellular automata; varying the objects or conditions likewise requires returning to these two steps to check what continues to hold. Lean can verify formal deductions, while human understanding enables pivotal methods to be interpreted, modified, and transferred—which is precisely the work the advisory group insists on supporting. At the same time, "releasing research results" and "opening research tools" remain two distinct matters: the internal model that generated the papers has not been made public, and mathematicians cannot directly reuse the same tool to reproduce reasoning or explore other topics.

In response to concerns from the academic community, OpenAI outlined a series of ongoing initiatives, including exploring community-hosted repository options, refining precursor citations and readability explanations in subsequent revisions, funding relevant workshops to assist in digesting key results, and stating that it is working toward a responsible public release of the model. Transitioning from publicly released candidate results into genuinely verifiable, explainable, and extendable mathematical knowledge will require these manuscripts to undergo rigorous, long-term digestion and scrutiny by the scientific community.