On August 1, 2026, OpenAI published Ten advances in mathematics and theoretical computer science, a 249-page collection of research results produced by an internal version of Astra, its next major model. Every problem in the collection had been open with no progress on the main result for at least a decade, and most for far longer. The compute bill to find all ten solutions was roughly $2,000. That number, more than any individual theorem, is the part of this announcement that should stop you cold.

TLDR

OpenAI released ten new mathematical results generated by an unreleased internal model called Astra, spanning high-dimensional geometry, coding theory, group theory, operator algebras, arithmetic circuit complexity, quantum complexity, lattice cryptography, convex geometry, Ramsey theory and extremal combinatorics. The headline items include the first improvement since 1978 to the general high-dimensional sphere-packing exponent, the first improvements since 1977 and 1978 to the MRRW and Kabatianskii-Levenshtein bounds for binary and spherical codes, the construction of an explicit non-sofic group that kills the soficity conjecture, a disproof of Connes’s rigidity conjecture for property-(T) group von Neumann algebras, new circuit and formula lower bounds for the permanent, an exponential parallel repetition theorem for all two-player entangled quantum games that had been open since 2004, n^(1/400) hardness of approximation for the Euclidean closest vector problem via a direct 3SAT reduction that never invokes the PCP theorem, the sharp (n+1)^n/n! bound in Ehrhart’s volume conjecture in every dimension, a superexponential lower bound proving R_k(3) = k^Θ(k) and settling Erdős problem 183, and counterexamples to both the Erdős-Simonovits compactness conjecture and Erdős’s degeneracy conjecture. The model generated the arguments, humans prepared the manuscripts alongside the same model, and the model then formalized each argument in a Lean certificate, released publicly on GitHub together with narrated walkthroughs of the model’s reasoning. OpenAI explicitly declined to claim human authorship, framing attribution as a question the mathematical community has to answer and nodding to the signers of the Leiden Declaration on AI and Mathematics.

Thoughts

The $2,000 figure is the whole story compressed into four digits. A single one of these results, in the ordinary run of mathematics, represents a career milestone. The sphere-packing exponent had not moved since 1978. The MRRW coding bound had not moved since 1977. The soficity conjecture had been open since Gromov raised the approximation property in 1999 and Weiss named it in 2000, and the field’s best hope was a conditional route through permutation stability hypotheses that nobody had proved. Ten of these, at once, for the price of a used motorcycle. Whatever you believed about the trajectory of AI in research mathematics on July 31, the marginal cost of a decade-old open problem is now a number you can put on a purchase order.

What makes the collection hard to wave away is the Lean formalization. The standard and entirely reasonable objection to machine-generated mathematics is that a language model produces confident, fluent, subtly wrong arguments, and that checking them costs more expert time than they save. A Lean certificate collapses that objection. The proof either compiles against the kernel or it does not. OpenAI put the certificates in a public repository, which means the verification burden on the community is not “read 249 pages of von Neumann algebra and try to find the hole” but “run the checker.” That does not settle whether the arguments are illuminating, well-motivated, or the kind of mathematics anyone wanted. It does settle whether they are true, and that is the part people were most worried about.

Look at the actual character of the proofs and something more interesting shows up than “the machine brute-forced it.” The closest vector problem result gets n^(1/400) hardness through a direct reduction from 3SAT using Reed-Solomon power-sum constraints over a characteristic-two field, and it deliberately does not route through the PCP theorem or the Projection Games Conjecture. That is a structurally unusual choice, the kind a human specialist might avoid because the field’s toolkit points elsewhere. The Ehrhart proof imports Bergman kernels and Berndtsson’s positivity theorem from complex geometry to settle a lattice-point question in convex geometry. The Ramsey result adapts saturated-matrix machinery originally built for zero-error list decoding. These are cross-domain transplants. Whatever Astra is doing, it appears to be less constrained by disciplinary habit than the people who have been staring at these problems.

OpenAI’s attribution paragraph deserves more attention than it will get. The company states flatly that claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work. That is a real position, taken at a moment when the commercially convenient move would have been to blur the line, list a few human co-authors, and let the papers slide into journals with the usual byline. Instead they named the model as the source of the arguments and kept responsibility for correctness. Compare that to the flood of quietly AI-assisted preprints already circulating with no disclosure at all, and OpenAI’s posture is the more honest one. The Leiden Declaration, published in June 2026 and endorsed by the International Mathematical Union, exists precisely because the community saw this coming and wanted values stated before the fact rather than after.

The uncomfortable question the release does not answer is what mathematicians are for now. Erdős offered $250 for the value of the multicolor Ramsey limit and $100 for merely deciding whether it was finite. Those prizes encoded a belief about how hard the problem was and how long it would take a human community to get there. A model settled the finiteness question for a rounding error on an API bill. The optimistic reading, and OpenAI leans on it, is that these results are seeds: the community engages with them, places them in context, and builds new research on the ideas. The pessimistic reading is that “engaging deeply with the results” is a demotion from producing them. My guess is that the honest answer is neither, and that mathematics becomes a field where taste, problem selection and interpretation are the scarce human contributions while derivation is not. That is a smaller job than the one mathematicians signed up for, and it is still a real one.

Key Takeaways

• OpenAI published ten new results in mathematics and theoretical computer science on August 1, 2026, all generated by an internal version of Astra, its next major model, which has not been publicly released.
• Every problem in the collection had been open with no progress on the main result for at least ten years, and in most cases for considerably longer than that.
• The total token cost to find all ten solutions would have been roughly $2,000 at Sol API rates, a figure OpenAI disclosed directly in the announcement.
• The workflow was three-stage: the model generated the mathematical arguments, humans prepared the arguments into manuscripts with help from the same model, and the model then formalized each argument as a Lean certificate.
• The Lean 4 formalizations are published in a public GitHub repository at openai/ten-proofs, so any reader can machine-check the proofs rather than take the claims on trust.
• OpenAI also released a narration of the model’s thinking process for each of the ten solutions, described as reasoning walkthroughs.
• Result 1, high-dimensional sphere packing: the exact exponential decay rate of the Cohn-Elkies linear program is determined, giving LP_d^(1/d) converging to sqrt(e/2π) and the density bound Δ_d ≤ 2^(-(0.6044…+o(1))d).
• That sphere-packing exponent is the first improvement since 1978, when Kabatianskii and Levenshtein established 0.59905576, with subsequent work improving only lower-order factors.
• The matching lower bound in the same chapter proves that no Cohn-Elkies auxiliary function can ever improve the exponent further, which closes the method rather than merely advancing it.
• The same chapter settles the Fourier sign-uncertainty problem asymptotically, proving that both the positive and negative eigenvalue uncertainty radii are (1/π + o(1))·sqrt(d), confirming a conjecture of Cohn and Gonçalves.
• Result 2, binary and spherical codes: exponentially improved upper bounds on the maximum size of binary codes at any prescribed minimum distance, plus analogous results for high-dimensional spherical codes.
• These are the first improvements to the general high-dimensional coding exponents since the McEliece-Rodemich-Rumsey-Welch bound of 1977 and the Kabatianskii-Levenshtein bound of 1978.
• The coding technique attaches a moving subspace to each code point rather than a single vector, producing scalar two-point certificates whose strength scales with the projection rank D/d_E.
• Result 3, non-sofic groups: the unit group of the binary Leavitt algebra over the two-element field is proved not sofic, disproving the soficity conjecture outright.
• Soficity asks whether every finite piece of a countable group’s multiplication table can be approximated by permutations of a finite set, a property Gromov introduced in 1999 and Weiss named in 2000.
• Prior routes to a non-sofic group all required unproved permutation-stability hypotheses. This proof requires none of them.
• The soficity proof combines Kun’s expander decomposition for property-(T) groups, the Kun-Thom centralizer obstruction, and a contradiction forcing Thompson’s group V to be locally embeddable into finite groups.
• Result 4, Connes’s rigidity conjecture: infinitely many pairwise nonisomorphic, mutually commensurable, finitely generated ICC property-(T) groups are constructed sharing a single group von Neumann algebra.
• Connes posed the conjecture in his 1994 monograph as Problem 1, asking whether the group factor of an ICC property-(T) group determines the group up to isomorphism. It does not.
• The same construction answers Popa’s finite-to-one question in the negative and shows his countable-to-one bound from the 2006 Madrid ICM address is sharp.
• The trick behind the counterexample is elementary in outline: binary carry puts different compact abelian group structures on the same probability space with the same Haar measure and the same group action.
• Result 5, arithmetic circuit complexity: division-free circuits computing the n by n permanent require Ω(n^2 log log n) gates, breaking through the trivial Ω(n^2) barrier.
• Arithmetic formulas for the permanent require Ω(n^4 / log n) variable-labeled leaves, improving the classical Ω(n^3) bound, and the result survives even when division is allowed.
• The circuit bound works by constructing an affine specialization whose gradient vanishes on a low-dimensional set, then applying Bézout’s inequality against reverse-mode differentiation.
• The paper explicitly explains why both arguments exploit properties specific to the permanent and do not transfer to the determinant, which is important because the determinant has polynomial-size circuits.
• Result 6, quantum parallel repetition: exponential decay is proved for every finite two-player entangled game with entangled value below 1, resolving the quantum analogue of Raz’s 1995 theorem.
• The quantum question was noted as open by 2004. Yuen proved only polynomial decay in 2016, and Bavarian, Vidick and Yuen got exponential decay only for anchored games obtained by modifying the original game.
• The new bound is exp(-c·ε^13/(ε + log|A||B|)·n), and the paper concedes the exponent 13 is almost certainly not optimal while insisting the qualitative exponential decay is the point.
• The key new ingredient is a postselection-stable quantum sampleability estimate that avoids the inverse dependence on the conditioning event probability that blocked earlier attempts.
• Result 7, closest vector problem: a deterministic polynomial-time many-one reduction from 3SAT gives n^(1/400)-factor hardness for the Euclidean closest vector problem.
• The reduction uses no randomization, no gap-producing PCP, and no Projection Games Conjecture, which makes it methodologically unusual for a hardness-of-approximation result of this strength.
• The same construction yields n^(1/200) hardness for binary nearest codeword and syndrome decoding, and n^(1/(200p)) for closest vector in every fixed rational ℓ_p norm.
• Lattice problems underpin NIST-standardized post-quantum key encapsulation and digital signatures, so results mapping which approximation regimes remain intractable have direct relevance to deployed cryptography.
• Result 8, Ehrhart’s volume conjecture: the sharp bound (n+1)^n/n! is proved in every dimension for convex bodies whose barycenter is their only interior lattice point.
• Ehrhart asked the question in 1964 and proved it only for planar bodies and for simplices. The best prior general bound was roughly 4^n·e^(-cn), which is exponentially far from sharp.
• The Ehrhart proof runs through complex geometry, using Berman-Berndtsson transport, lattice Bergman spaces, and Berndtsson’s positivity theorem to make a partition-function logarithm convex.
• Result 9, multicolor Ramsey numbers: R_k(3) ≥ (c·k^(1/3)/log k)^k, which combined with the classical factorial upper bound establishes R_k(3) = k^Θ(k).
• The previous best lower bound was 380^(k/5), merely exponential. The gap between exponential lower bounds and factorial upper bounds had been highlighted repeatedly by Conlon, Fox and Sudakov.
• Erdős offered $250 for determining the growth limit and $100 for merely deciding whether it is finite. The new result shows the limit is infinite, settling Erdős problem 183.
• A direct corollary: the Shannon capacity of graphs with independence number 2 is unbounded, so Shannon capacity cannot be bounded above by any function of the independence number.
• Result 10, extremal graph theory: a finite family of connected bipartite graphs is constructed with ex(n, F) = O(n^(4/3 – 1/48)) while every individual member has ex(n, F) = Ω(n^(4/3)), disproving the Erdős-Simonovits compactness conjecture.
• A second construction gives a fixed connected bipartite 2-degenerate graph H with ex(n, H) ≥ c·n^(3/2+ε), disproving Erdős’s degeneracy conjecture at r = 2 and refuting a related implication Janzer’s 2023 work had left open.
• This is not OpenAI’s first mathematical result. In May 2026 the company shared an AI-generated disproof of the Erdős unit-distance conjecture, found while evaluating an unreleased model.
• That May disproof has already generated follow-on human research, including work by Bloom, Sawin, Schildkraut and Zhelezov showing the sum-product conjecture is false for real numbers, and papers by Pohoata, by Saha, Xu and Ye, by Goh and Hatami, and by Lee, Pohoata and Zhu.
• OpenAI states that attribution should honestly reflect how a result was produced, and explicitly refuses to claim human authorship for proofs its system generated.
• The announcement names the Leiden Declaration on AI and Mathematics, published June 2026 and endorsed by the International Mathematical Union, and says OpenAI has deep respect for those concerned about AI’s impact on the field.
• The release is paired with ChatGPT for Academic Researchers, an initiative providing 100,000 scientists and mathematicians with free access to OpenAI’s best models.
• Sebastien Bubeck, announcing the work publicly, framed it as ten Astra proofs released complete with Lean certificates and chain-of-thought walkthroughs for each.

Detailed Summary

What OpenAI actually released and how it was produced

The publication is a 249-page document titled Ten Advances in Mathematics and Theoretical Computer Science, authored by OpenAI and subtitled as a collection of research papers by an internal model. Each of the ten results occupies its own chapter, complete with abstract, table of contents, full proof, and bibliography, formatted exactly as a standalone research paper would be. The pipeline OpenAI describes has three distinct steps and it matters that they are distinct. First, an internal version of Astra found the mathematical arguments while being evaluated on open research problems during development. Second, humans prepared those arguments into publishable manuscripts, working with the same model. Third, the model formalized each argument in Lean, producing certificates that OpenAI released alongside the paper in a public GitHub repository. On top of that, OpenAI published narrations of the model’s own reasoning process for each solution, which is the closest thing anyone has offered to an audit trail for machine-discovered mathematics.

The cost disclosure is unusual and deliberate. OpenAI states that the total tokens required to find these solutions would run roughly $2,000 at Sol API rates. Read that against the selection criterion, which is that every problem had seen no progress on its main result for at least a decade, and the implication is not subtle. The company is not claiming a lucky hit on a single famous conjecture. It is claiming that a decade-stale open problem in research mathematics now has a marginal discovery cost in the low hundreds of dollars, across eight distinct subfields simultaneously.

Sphere packing and the first movement of an exponent since 1978

Sphere packing asks how densely identical balls can fill Euclidean space. In dimensions 8 and 24 the answer is spectacular and known, thanks to Viazovska’s proof that the E8 lattice is optimal and the subsequent Leech lattice result by Cohn, Kumar, Miller, Radchenko and Viazovska. In high dimensions the picture has been much murkier. The Fourier-analytic linear programming method of Gorbachev and Cohn-Elkies gives an upper bound on density, and Cohn and Zhao proved it is always at least as strong as the classical Kabatianskii-Levenshtein spherical-code bound, but nobody knew whether it actually beat the classical exponent.

Chapter 1 answers that exactly. The linear program’s optimal density bound, taken to the d-th root, converges to sqrt(e/2π), confirming a conjecture of Afkhami-Jeddi, Cohn, Hartman, de Laat and Tajdini. In exponent terms the packing density is bounded by 2^(-(0.6044…+o(1))d), which beats the 1978 Kabatianskii-Levenshtein exponent of 0.59905576. That is the first improvement to the general high-dimensional sphere-packing exponent in 48 years. The result cuts both ways, though: the matching lower bound proves that no Cohn-Elkies auxiliary function can push the exponent further, so the method is now exhausted rather than merely advanced. The same chapter also nails the Fourier eigenfunction sign-uncertainty constants asymptotically, showing that both the positive and negative eigenvalue radii grow like sqrt(d)/π, which resolves a conjecture of Cohn and Gonçalves and connects to the spinless modular bootstrap in physics.

Codes, and a technique that moves the subspace with the point

Chapter 2 attacks the closely related question of how many codewords you can pack at a given minimum distance, for both binary codes on the Hamming cube and spherical codes on the sphere. The reigning general bounds are MRRW from 1977 for binary codes and Kabatianskii-Levenshtein from 1978 for spherical codes, both derived from Delsarte’s two-point linear programs. The new construction improves both exponents strictly, for every fixed relative distance and every fixed maximum inner product, which makes it the first improvement to either in nearly half a century.

The mechanism is worth understanding because it is conceptually clean. In the classical spectral construction, each retained harmonic space contributes a single vector attached to a code point. The new approach attaches an entire subspace to each point, living inside a common ambient space, and crucially the subspaces move with the points: any symmetry carrying point x to point y carries the subspace at x to the subspace at y. The overlap of the corresponding projections remains a scalar function of distance, so the certificate stays a two-point object rather than escalating to the matrix-valued three-point semidefinite programs of Bachoc and Vallentin. An exponentially large projection rank then improves the rate. As a bonus, taking the maximum inner product to 1 recovers the sphere-packing exponent of Chapter 1 as a limiting case, so the two results independently confirm each other.

Non-sofic groups and Connes’s rigidity conjecture

Chapters 3 and 4 are the two results most likely to reorganize their fields. A countable group is sofic if every finite portion of its multiplication table can be approximated by permutations of a finite set: multiplication holds almost everywhere and no nonidentity element fixes too much. Gromov introduced the property in his work on symbolic dynamics, Weiss named sofic groups and asked whether a non-sofic one exists, and the question calcified into the soficity conjecture. Chapter 3 constructs one explicitly, proving that the unit group of the binary Leavitt algebra over the two-element field is not sofic. Prior conditional routes, through flexible permutation stability of PSL_d(Z) or central extensions of p-adic lattices, all rested on hypotheses nobody had proved. This proof requires none, building instead on Kun’s expander decomposition for property-(T) groups and the Kun-Thom centralizer obstruction, then deriving a contradiction from the fact that elementary groups over the Leavitt algebra would force Thompson’s group V to be locally embeddable into finite groups.

Chapter 4 disproves Connes’s rigidity conjecture, which appeared as Problem 1 in his 1994 monograph and asked whether the group von Neumann algebra of an ICC property-(T) group determines the group. Property (T) was expected to prevent the collapse seen in the amenable case, where Connes’s classification theorem forces every amenable ICC group to share the hyperfinite II_1 factor. The counterexample constructs a countably infinite family of pairwise nonisomorphic, mutually commensurable, finitely generated ICC property-(T) groups all having the same group factor. The idea driving it is almost embarrassingly concrete: on the four-point probability space, coordinatewise addition gives the Klein four-group while a binary carry rule gives Z/4Z, and both carry the same uniform Haar measure. Globalize that carry and you get different compact group structures on one measured space with one group action, which the crossed product cannot distinguish. As a second consequence, Popa’s finite-to-one question is answered negatively and his countable-to-one bound from the Madrid ICM is shown to be sharp.

Complexity theory: the permanent, quantum games, and lattices

Chapter 5 attacks the central problem of algebraic complexity theory, whether the permanent admits polynomial-size arithmetic circuits. It does not settle that, but it moves two long-static bounds. For division-free circuits with unrestricted reuse of intermediate values, the permanent requires Ω(n^2 log log n) gates, which finally beats the trivial “it depends on all n^2 variables” bound. For formulas, it requires Ω(n^4 / log n) variable-labeled leaves, up from the classical Ω(n^3), and the bound survives when valid divisions are permitted. The circuit argument constructs an affine specialization of the permanent whose gradient vanishes on a small set, then plays Bézout’s inequality against the fact that reverse-mode differentiation computes a gradient with only a constant-factor blowup. The formula argument charges algebraically independent coefficients to distinct occurrences of selected variables and sums over entry-disjoint matchings. A full section is devoted to explaining why neither argument transfers to the determinant, which matters, because the determinant does have small circuits and any technique that proved otherwise would be wrong.

Chapter 6 resolves quantum parallel repetition. Raz proved in 1995 that repeating a classical two-player game n times in parallel drives the winning probability down exponentially whenever the original value is below 1. Whether the same holds when the players share entanglement was noted as open by 2004 and stayed open. Special classes fell along the way: XOR games, unique games, projection games, free games, anchored games. The general case did not. Yuen’s 2016 theorem gave polynomial rather than exponential decay. The new theorem gives exponential decay for every finite two-player one-round entangled game, with the rate depending on the soundness gap to the thirteenth power. The paper is candid that 13 is an artifact of a quantum correlated-sampling lemma and not the truth, and that the qualitative result is what matters. The technical unlock is a postselection-stable sampleability estimate that dodges the inverse dependence on the conditioning event’s probability.

Chapter 7 gives n^(1/400)-factor NP-hardness for approximating the Euclidean closest vector problem, along with n^(1/200) for binary nearest codeword and syndrome decoding, and n^(1/(200p)) for closest vector in any fixed rational ℓ_p norm. What distinguishes it is the route. Hardness-of-approximation results in this range normally go through the PCP theorem or assume the Projection Games Conjecture. This one is a direct, deterministic, many-one reduction from 3SAT, encoding assignments through Reed-Solomon power-sum constraints over a characteristic-two field and converting the resulting binary affine system into an integer lattice by coordinatewise reduction modulo two. Soundness comes from reconstructing separable root sets from power sums over a rational function field. Since lattice assumptions underpin the NIST post-quantum standards, mapping which approximation regimes stay intractable is not purely academic housekeeping.

Convex geometry, Ramsey numbers, and extremal graphs

Chapter 8 settles Ehrhart’s volume conjecture from 1964: among convex bodies whose barycenter is their only interior lattice point, the centered simplex maximizes volume, and the sharp bound is (n+1)^n/n! in every dimension. Ehrhart himself got the planar case and the simplex case. For general centered bodies the best available was roughly 4^n with progressively better subexponential corrections, most recently combining work of Campos, van Hintum, Morris and Tiba with Klartag and Lehec’s solution of Bourgain’s slicing problem, still leaving an exponential gap. The proof imports machinery from complex geometry. A Berman-Berndtsson transport potential turns the body into a weighted space on the complex torus, the unique-interior-lattice-point hypothesis becomes the statement that a certain holomorphic space contains only constants, a filtration by vanishing order at a fixed point produces a ray of potentials, and Berndtsson’s positivity theorem makes the log partition function convex. Bounding its initial slope from both sides pins the constant.

Chapter 9 proves that the multicolor Ramsey number for triangles grows superexponentially: R_k(3) is at least (c·k^(1/3)/log k)^k, which together with the classical factorial upper bound gives R_k(3) = k^Θ(k) and shows the limit of R_k(3)^(1/k) is infinite. Prior lower bounds came from tensoring small triangle-free colorings and sum-free partitions, topping out at 380^(k/5), merely exponential. Graham, Rothschild and Spencer recorded the superexponential growth question in Ramsey Theory, Conlon, Fox and Sudakov highlighted the gap, and Erdős attached prize money: $250 for the limit’s value, $100 for deciding whether it is finite. The construction adapts random-matrix and coordinate-covering ingredients from Alon, Ben-Eliezer, Shangguan and Tamo, themselves descended from zero-error list decoding work, and builds the coloring recursively with palettes recording which colors are missing from each block. The Ramsey-Shannon correspondence then delivers a striking corollary: there are graphs with independence number 2 and arbitrarily large Shannon capacity, so Shannon capacity is not bounded by any function of the independence number.

Chapter 10 delivers two counterexamples in extremal graph theory. The Erdős-Simonovits compactness conjecture asks whether forbidding a finite family of graphs, each containing a cycle, can reduce the extremal number by more than a constant factor relative to forbidding some individual member. The answer is yes: a family built from subdivided complete bipartite templates has ex(n, F) = O(n^(4/3 – 1/48)) while every member individually has ex(n, F) = Ω(n^(4/3)), with the lower bounds coming from incidence graphs of generalized quadrangles. Separately, Erdős conjectured that every fixed bipartite r-degenerate graph satisfies ex(n, H) = O(n^(2 – 1/r)). A layered construction, with a vertex adjoined for every pair in the preceding layer, plus a sampled Hamming-distance bipartite graph and an entropy potential argument, produces a 2-degenerate H with ex(n, H) ≥ c·n^(3/2+ε). That kills the r = 2 case and also refutes the forward implication of a related Erdős conjecture that Janzer had only partially addressed in 2023.

The attribution question OpenAI chose to raise

The section OpenAI titled “Responsibility to the mathematical community” is short and unusually direct. It acknowledges that systems capable of contributing to mathematical research raise questions a technology company cannot answer alone, and it names the signers of the Leiden Declaration on AI and Mathematics as people whose concerns the company respects. The declaration, published in June 2026 out of a 2025 Lorentz Center workshop at Leiden University, was authored by sixteen mathematicians, signed by roughly fifteen hundred people, and endorsed by the International Mathematical Union. It exists because the community anticipated exactly this moment.

OpenAI’s stated position is that attribution should reflect how a result was actually produced, and that claiming human authorship for a machine-generated proof would misrepresent both sides of the ledger. The company takes responsibility for correctness, having helped prepare the manuscripts and formalize the proofs, while assigning the mathematical arguments to the system. It then asks the community to engage with the results, contextualize them, and build on the ideas. Pair that with ChatGPT for Academic Researchers, which puts free access to OpenAI’s best models in the hands of 100,000 scientists and mathematicians, and the strategy is legible: publish the results with verifiable certificates, decline the authorship credit, and distribute the tool broadly enough that the field adapts around it rather than against it.

Notable Quotes

“Today, we are sharing a selection of ten results to problems that have been open and have seen no progress on the main result for at least a decade, and in most cases much longer.”

OpenAI, setting the selection criterion for the ten problems

“The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates.”

OpenAI, disclosing the compute cost of ten decade-old open problems

“We believe attribution should honestly reflect how a result was produced: claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.”

OpenAI, on why the papers do not carry human bylines

“We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness, while the mathematical arguments themselves were generated by our system.”

OpenAI, drawing the line between human contribution and machine contribution

“The emergence of systems capable of contributing to mathematical research raises questions that cannot be answered by a technology company alone.”

OpenAI, opening its section on responsibility to the mathematical community

“This is the first improvement since 1978 to the general sphere-packing exponent.”

Chapter 1 of the paper, on a bound that had not moved in 48 years

“These are the first improvements to the respective general high-dimensional exponents since 1977 and 1978.”

Chapter 2, on the binary and spherical code bounds

“The central point is that the decay is exponential for every finite entangled game.”

Chapter 6, conceding that the exponent 13 is not optimal while defending the result

“In particular, the Shannon capacity of graphs with independence number 2 is unbounded.”

Chapter 9, on the information-theory corollary of the Ramsey lower bound

“We hope the mathematical community will engage deeply with these results, place them in context, and bring the ideas behind them to life through new research and discovery.”

OpenAI, closing the announcement

Read the full announcement at OpenAI’s publication page, and check the proofs yourself: the Lean 4 certificates for all ten results are public.

Related Reading

• openai/ten-proofs on GitHub the Lean 4 formalizations of all ten results, so you can machine-check the claims instead of trusting them.
• The Leiden Declaration on Artificial Intelligence and Mathematics the June 2026 statement OpenAI cites, authored by sixteen mathematicians and endorsed by the International Mathematical Union.
• Erdős problem 183 the multicolor Ramsey question settled by Chapter 9, with the original prize offers and full history.
• Lean the proof assistant and programming language whose kernel is what actually certifies these arguments.
• Sphere packing (Wikipedia) background on the problem whose high-dimensional exponent had not moved since 1978.
• Noncommutative Geometry by Alain Connes, the 1994 monograph where the rigidity conjecture disproved in Chapter 4 appears as Problem 1.