OpenAI says its unreleased Astra model solved 10 math problems that had stood open for decades
The reasoning cost was about $2,000. All 470,000 lines of proof are open source and have been machine-checked. These results offer the first glimpse of what the unreleased model can do.
- OpenAI says an unreleased model solved 10 long-standing problems in mathematics and theoretical computer science. The oldest was posed in 1964.
- These problems demand different kinds of mathematical work. The hardest require constructing entirely new mathematical objects.
- All 470,000 lines of proof are open source, and machines have checked the logic line by line. But machines still cannot verify either end of the chain.
An unreleased model tackled 10 problems that had stood for decades
OpenAI unexpectedly released an announcement and a paper of more than 200 pages claiming that an internal version of its next flagship model had solved 10 long-standing problems in mathematics and theoretical computer science. These are not contest exercises. The oldest was posed in 1964, and even the newest had remained open for more than 20 years. They span eight largely unrelated fields. The results also require very different kinds of mathematical work: some push forward bounds that had not budged in decades, while others construct counterexamples no one had ever seen—a task long considered among the hardest to teach a machine.
The model is called Astra. It is OpenAI's unreleased next-generation flagship model, and these results came from an internal version.
The cost was strikingly low: OpenAI says that, at Sol API rates, the tokens used to solve these 10 major problems would cost only about $2,000—negligible compared with conventional research spending.
Here is when the problems were first posed:
The years when the problems behind these 10 results were posed. There are 11 points because the extremal graph theory result covers two conjectures: degeneracy from 1967 and compactness from 1982. The horizontal axis is proportional to time. The 1977 and 1978 points, and the 1994 and 1995 points, nearly overlap because each pair is only one year apart. Dates come from the chapter introductions in the 249-page paper and the Erdős Problems database.
What we know about Astra so far
Astra has not been released, and public information is scarce.
Positioning: It is a new model class in OpenAI's next-generation flagship family, alongside Sol, Terra, and Luna. Whether it will eventually be called GPT-6, GPT-5.7, or something else remains undecided. There is no release date.
Core capability: It is reportedly designed to coordinate multiple agents and work continuously for hours or even days on unusually complex, long-horizon problems. OpenAI's cited use cases are complex projects and advanced mathematics. Sam Altman has already demonstrated it to politicians and regulators in Washington.
The unresolved weakness: Long-running workflows accumulate errors. Whether a system can recognize when it has gone off track and recover remains a widely acknowledged weakness in this class of system. Multiple agents can also perform worse than one on tightly coupled tasks because of coordination overhead. There is no public evidence showing how reliably Astra handles these problems. These 10 math results are its only public record.
The details above come from The Information, which cited three people familiar with the matter. They are not part of an official OpenAI announcement; we encountered them through The Decoder's reporting. OpenAI's announcement never uses the name "Astra," referring only to "an internal version of our next flagship model." OpenAI researcher Noam Brown identified the model as Astra on X the day of the announcement.
All 10 results at a glance
Here is what each result changes.
| Field | What changed | How long it stood |
|---|---|---|
| High-dimensional geometry | Pinned the exponent for the sphere-packing upper bound at exactly 0.6044 | Since 1978 |
| Coding theory | Exponentially lowered the upper bounds for binary and spherical codes | Since 1977 / 1978 |
| Convex geometry | Proved the exact upper bound in every dimension for the Ehrhart volume conjecture | Posed in 1964 |
| Algebraic complexity | Raised both circuit and formula lower bounds for the permanent | The field's central problem |
| Quantum complexity | Established exponential parallel repetition for every two-player entangled game | Raz's 1995 classical result |
| Lattice cryptography | Reached a fixed polynomial hardness factor n^(1/400) for CVP for the first time | Since 2003 |
| Group theory | Constructed the first non-sofic group | Asked by Weiss in 2000 |
| Operator algebras | Disproved Connes' rigidity conjecture | Problem 1 in a 1994 monograph |
| Extremal combinatorics | Disproved the compactness and degeneracy conjectures | 1982 / 1967 |
| Extremal combinatorics | Pinned multicolor Ramsey growth in k at Θ(k) | Erdős Problem 183 |
We checked the "How long it stood" column against the chapter introductions in the 249-page paper and the Erdős Problems database. The two extremal-combinatorics rows together count as the tenth item in OpenAI's tally, so the table's 10 rows correspond to 10 reported advances.
The results fall into three broad categories of mathematical work. The first pushes forward a bound that had not moved in decades. The second determines whether something can be computed or broken. The third constructs a counterexample from scratch and uses it to kill a conjecture outright.
Tightening bounds that stood for decades
The first three problems ask the same basic question: how much can fit inside a constrained space?
High-dimensional sphere packing
Record unchanged since 1978How densely can equal-sized spheres fill a space? In two dimensions, it is like arranging coins on a table: the optimal pattern covers 90.7% of the surface. In three dimensions, it is like stacking oranges at a market stall: the limit is 74%. Both results have rigorous proofs. Exact answers for dimensions 8 and 24 were also found in the past decade, and Maryna Viazovska won the 2022 Fields Medal in part for solving the 8-dimensional case.
In high-dimensional spaces, however, we cannot even visualize the geometry. We can only estimate an upper bound—and it is counterintuitively low: in a 100-dimensional space, spheres can occupy less than one quintillionth of the total volume.As the dimension rises, space becomes increasingly "empty," with the gaps between spheres consuming almost all the volume.
An exponent measures how quickly this upper bound falls with dimension. A larger exponent means faster decay and a tighter upper bound. This result calculates the exact exponent achievable by the Cohn–Elkies method: 0.6044…
The key step
The Cohn–Elkies method translates "how densely can spheres be packed?" into a function-construction problem. Build a function that is nonpositive beyond radius 1 while its Fourier transform is nonnegative everywhere. Each such function yields a density upper bound; the cleverer the function, the tighter the bound. For 48 years, no one knew the inherent limit of the method.
The new approach starts with a Gaussian function. Its Fourier transform is itself, so it has the required symmetry built in. Unfortunately, the critical radius that determines success lands in the wrong place. The researchers multiply it by a carefully designed even function, shifting the critical radius where it needs to go without disturbing the symmetry. The required shift is exactly ½·log2, derived from a 17th-century product formula due to Wallis.
After the shift, the radius matches the value predicted by an independent Mellin-reflection argument. One side constructs a function and establishes the upper bound; the other proves no better function can exist. Together, they pin down the limit of the method.
The previous record was 0.59905576…, set by Kabatianskii and Levenshtein in 1978. Later work improved only lower-order factors; no one moved the exponent for 48 years. The difference between 0.599 and 0.604 looks tiny, but it sits in an exponent. In 1,000 dimensions, the new upper bound is about 40 times tighter. And this is more than an incremental improvement: the result also proves that no auxiliary function within this method can go any further.
Maximum sphere-packing density by dimension (log-scale bars)
The two dark rows are the only dimensions for which humans know the exact answer: dimension 8 (Viazovska, 2016) and dimension 24. Everything above that—including the new result—is only an upper bound. The true values remain unknown. The 100-dimensional row uses the new exponent. The bars use a logarithmic scale; otherwise the later rows would be too short to see.
Values come from Chapter 1 of the paper. The number line is proportional to the actual values, so the distance between the points represents the real numerical difference.
Binary and spherical codes
Records unchanged since 1977 / 1978A scratched CD can still play, a weak phone signal can remain intelligible, and a QR code with a missing corner can still scan because of error-correcting codes. The message is encoded as a string of 0s and 1s, with every pair of valid strings required to differ in at least a certain number of positions. Greater separation makes errors easier to recover from, but it also leaves fewer valid strings and lowers the amount of information the channel can carry.
The central question is therefore: once error tolerance is fixed, how many valid strings can remain? That number is the efficiency ceiling of a channel. The new result lowers this ceiling exponentially at every fixed distance. It does the same for the corresponding problem on a sphere.
The key step
The classical bound, known as the MRRW bound, comes from a fixed spectral curve. The new method adds a degree of freedom: the curve can move. The researchers' first recurrence relation was wrong, and the walkthrough devotes an entire section to explaining why.
After fixing it, the researchers found that this improvement alone still could not beat the optimized classical bound. Near relative distance 0.1, the new algorithm gave 0.700 while the classical bound gave 0.693—worse, not better. So they constructed an entire family organized by weight layers: constrain the code to a shell of fixed weight, then let the stabilizer symmetry group act separately on that shell and its complement. The result is a full hierarchy, not merely an improved polynomial. That is what finally beats the old bound at every distance.
The paper describes this as the first improvement since 1977 and 1978 to the general high-dimensional exponents in the two respective fields. In the limit as the distance approaches zero, the spherical-code construction also rederives the optimal sphere-packing exponent above. Two apparently unrelated problems turn out to share the same underlying structure.
Ehrhart volume conjecture
Posed in 1964, open for 62 yearsImagine a room filled with a three-dimensional grid of points spaced one meter apart across the floor and through the air. You inflate a balloon inside it. The balloon may have any convex shape—no inward dents—but it must satisfy two rules: its center of mass lies exactly on a grid point, and apart from that point, its interior may not contain any other grid point.
How large can the balloon become? In three dimensions, the answer is 64/6, about 10.7 grid-cell volumes. Ehrhart conjectured in 1964 that, in every dimension, the largest shape is a particular simplex. The new work proves the conjectured exact upper bound in every dimension: (n+1)ⁿ / n!
The key step
The proof recasts the geometry problem in complex analysis. Earlier approaches required the shape to be "rational," meaning all vertex coordinates were fractions, because only then could they connect to the machinery of algebraic geometry. The breakthrough is the realization that this assumption is unnecessary. Any centered convex body can be turned directly into a potential function, moving the entire problem onto a complex torus.
The cost is that every part of the analysis must genuinely work on a noncompact space; compactness can no longer be used as a shortcut. The researchers also abandoned a lengthy route based on harmonic symmetrization, documented in the walkthrough.
Ehrhart himself proved only the planar case and the simplex case in every dimension. For general convex bodies, the previous upper bound was on the order of 4ⁿ. In dimension 10, that old bound was roughly 147 times looser than the true value.
Deciding what can—and cannot—be computed
The second category shifts from packing limits to computational tractability. These problems ask what can be computed efficiently and what can be made computationally intractable, bringing them closest to computer science and cryptography.
The permanent: almost the determinant, but vastly harder
The permanent here is the permanent, not a matrix product—a common mistranslation in Chinese summaries.
Here is one way to understand it. Suppose n people must be assigned to n jobs, and every person has a score for every job. List every possible one-person-per-job assignment. For each assignment, multiply its n scores, then add the products across all assignments. That is the permanent. The determinant uses the same formula, except that half the assignments receive a minus sign.
Determinant
det(X) = Σ sgn(σ) · Π xᵢ,σ(ᵢ)
A laptop can compute the determinant of a 1,000-by-1,000 matrix in seconds with Gaussian elimination, using roughly one billion steps. The algorithm has existed for two centuries.
Permanent
per(X) = Σ Π xᵢ,σ(ᵢ)
Remove the sign, and the best known algorithm must examine 2 to the n combinations. At size 50, that is more than one quadrillion steps—far beyond a laptop.
Removing the alternating signs turns an expression computable in seconds into an intractable one. No one fully understands why. In 1979, Valiant proved that the permanent is VNP-complete, placing it at the top of a vast class of counting problems: if anyone finds a polynomial-size expression for computing it, a large part of algebraic complexity theory collapses. It is the algebraic analogue of P versus NP.
The key step
The proof has two stages: first construct many useful small components, then combine them into one large object. Multiplication fails because a single zero component collapses the whole product. They must be added, so their individual contributions accumulate.
The difficult part is making a single permanent substitution implement exactly that addition. The answer is to use roots of unity—equally spaced points on the unit circle in the complex plane—to arrange the constant columns. This makes every cross-component pairing cancel algebraically, leaving only each component's internal contribution. The cancellation is already visible in a fourth-order example: the mixed block evaluates to exactly zero.
The central problem remains unsolved. But the new work raises the lower bound on how large a computation must be: division-free arithmetic circuits require at least Ω(n²·log log n) gates, and arithmetic formulas require at least Ω(n⁴/log n) leaves. The latter still holds when division is allowed, provided the denominator is not identically zero. Such lower bounds are the only way to approach the central question from the other side: every increase narrows the remaining possibility that the permanent is secretly easy to compute.
Quantum parallel repetition
Classical result from 1995; quantum case openTwo suspects are questioned separately after coordinating their stories in advance. They might bluff their way through one round. But if the same test is asked n times in parallel, with every answer required to match, how quickly does their chance of success fall?
Raz proved in 1995 that if they cannot succeed with certainty in one round, their success probability falls exponentially after n repetitions. This theorem guarantees that repeating a somewhat unreliable test can make it extremely reliable. Modern cryptographic protocols and verifiable computation rely on that principle.
The trouble begins with quantum mechanics. Replace the suspects' shared plan with quantum entanglement—a correlation with no classical counterpart that can keep their separated answers aligned. Does the same guarantee survive? The problem remained open for 30 years. The new work proves exponential decay for every finite two-player entangled game.
The key step
A step in the classical proof takes a square root. In the quantum setting, that breaks: the derivative of an operator's square root diverges at very small eigenvalues, while the coefficients in a quantum strategy can be arbitrarily small. This is not a harmless constant that can be ignored.
The principle that survives is: preserve the quantum probability itself while spreading out the troublesome eigenvalue scales. The first version did this by averaging imaginary powers; it was later replaced with a simpler approach. The walkthrough stresses one point that cannot be relaxed: the operations here do not commute. Treating the products like ordinary numbers and changing their order leads straight back to the invalid proof.
The strongest prior general result, proved by Yuen in 2016, established only polynomial decay. Exponential decay had previously been known only for a few special classes of games.
Closest Vector Problem (CVP)
Last advance in 2003Imagine an infinite city whose intersections do not follow a north-south grid, but a skewed and stretched lattice. Given any point in the city, find its nearest intersection. In two dimensions, you can often see the answer immediately. In hundreds of dimensions, no fast method is known.
That difficulty makes lattice problems a foundation of post-quantum cryptography. The quantum-resistant encryption algorithms standardized by the U.S. National Institute of Standards and Technology rely on this family of problems. So proving the problem harder is good news for cryptography, not bad news: every proof that even approximation is impossible adds another theoretical layer beneath the encryption.
The new result gives a direct reduction from 3SAT and proves that approximating CVP within a factor of n^(1/400) remains NP-hard. This is the first fixed polynomial factor.
The key step
The project first took a long detour through signed multivariate moment histograms, which the walkthrough records candidly. The final approach encodes a 3SAT assignment using power sums. Instead of recording the numbers themselves, it records the sum of their first powers, second powers, third powers, and so on. The original multiset can be recovered from this sequence of power sums through Hankel reconstruction, even over fields of characteristic two.
Shifted moments then convert "every clause is satisfied" into the property that one global algebraic root satisfies all clauses simultaneously. The entire reduction avoids randomness, the probabilistically checkable proof (PCP) theorem, and the Projection Games Conjecture. That is unusual for this kind of hardness proof, where earlier routes almost always relied on PCP machinery.
The previous best result, by Dinur, Kindler, Raz, and Safra in 2003, was n^(a/log log n). Although that factor grows faster than any power of log n, its exponent approaches zero, so it never reaches a fixed n^c. The new reduction is also fully deterministic, uses no PCP theorem, and does not depend on the Projection Games Conjecture. ⚠️ One necessary qualification: the paper explicitly notes that deployed cryptographic algorithms rely on average-case hardness and structured assumptions, not directly on worst-case NP-hardness for CVP. This result draws a theoretical boundary; it does not certify the security of existing algorithms.
Constructing a counterexample no one had ever seen
The third category is the genuinely difficult one. The first two push along a line whose direction is already known. This category has to create something from nothing: imagine a mathematical object that has never existed before, then prove that it exists and simultaneously satisfies several conflicting conditions. Four results fall into this category, and three of them directly overturn conjectures that had circulated for decades.
A non-sofic group
Asked by Weiss in 2000, open for 26 yearsA "group" can be understood as a collection of actions and the rules for composing them. Think of every possible move of a Rubik's Cube: performing two turns may equal some other turn, and together these relationships form an enormous rulebook. Some groups are infinite, so their rulebooks are infinite too.
Calling a group sofic means that no matter which small piece you cut from this infinite rulebook, you can find a finite deck of cards and define a set of shuffles that reproduces that fragment with arbitrary accuracy. A finite object that fits on a table can simulate part of an infinite structure. Larger fragments require more cards, but some finite deck always works.
Gromov introduced the property in 1999. Weiss named it in 2000 and asked the decisive question: does any group resist every such finite approximation, no matter how you cut it or how many cards you use? The new work constructs one directly.
The key step
The challenge is to place two conflicting ingredients inside the same structure: one must create an obstruction that cannot be approximated away, while the other must derive a contradiction from the assumption that approximation is possible. Earlier attempts always left a gap through which the defect escaped.
The new stage is an algebra that contains a copy of itself: the binary Leavitt algebra. This ring is exactly isomorphic to its own 2×2 matrix ring, so the entire structure can be embedded intact inside one of its own corners without losing a single coefficient. That self-similarity allows a rigid group with property (T) and Thompson's group V to coexist in the same ring for the first time. The former supplies the obstruction; the latter supplies the contradiction.
Why this existence result matters: for more than 20 years, many theorems were written as "true for all sofic groups." Because no counterexample existed, people often treated that as roughly equivalent to "true for all groups." Now there is a counterexample, and those theorems have a real boundary for the first time. Every previous route was conditional: assume a group had some stability property, then infer the existence of a non-sofic group. This construction is unconditional.
Connes' rigidity conjecture
Problem 1 in the 1994 monographA group can be used to construct an object called a group von Neumann algebra. Think of the transformation as taking an X-ray of a machine: the colors, materials, and serial numbers of its parts disappear, leaving only the skeleton of how the parts engage. The names and shapes of the original elements vanish. What remains is the relational structure among the operations.
Connes conjectured that for a particularly "rigid" class of groups—those with infinite conjugacy classes and Kazhdan's property (T)—this X-ray would be enough to reconstruct the original machine uniquely. If two groups produced the same image, they would have to be the same group.
The new work constructs infinitely many pairwise nonisomorphic groups that produce the same image. The conjecture is false.
The key step
The construction uses something taught in elementary school: carrying in binary addition.
On exactly the same set of coordinates, the researchers define two different addition laws. One uses ordinary digitwise addition; the other adds a carry term. The two laws inhabit the same space with the same probability measure, and from a random perspective they look identical.
The carry is completely invisible to the measurable side, yet perfectly visible to the discrete side. The X-ray captures only the measurable side, so the two groups produce the same image. But the groups themselves live on the discrete side, where they are genuinely different. The conjecture fails in that gap.
Questions about whether an invariant uniquely determines its original object are among the most common in mathematics. A "no" means this X-ray discards more information than mathematicians had believed for decades. The conjecture grew out of Connes' 1980 rigidity theorem, took shape in the proceedings of a 1982 Kingston conference, and appeared explicitly as Problem 1 in his 1994 monograph. The new result also rules out a related "finite-to-one" question posed by Popa.
Two conjectures in extremal graph theory
1967 and 1982; Erdős Problems 146 and 180At a party of n people, every pair may shake hands or not. Now impose a restriction, such as "no four people may form a cycle of handshakes." What is the largest number of handshakes still possible? That is the kind of question extremal graph theory asks. If four-person cycles are forbidden, the answer is roughly half of n to the power 1.5. At a party of 100 people, there can be about 500 handshakes, compared with 4950 without restrictions. The stronger the restriction, the fewer handshakes remain; the field studies the precise relationship between the two.
The compactness conjecture of Erdős and Simonovits from 1982 asks whether, when several patterns are forbidden at once, one of them always dominates—so forbidding that single pattern is effectively as strong as forbidding the whole family. The new work constructs a family of graphs for which forbidding the entire family leaves only O(n^(4/3−1/48)) handshakes, while forbidding any single member still permits Ω(n^(4/3)). The gap is a polynomial factor of n^(1/48), far beyond any constant factor.
The degeneracy conjecture, posed by Erdős in 1967, gives a formula that predicts the upper bound from "how sparse the graph is." The new work constructs a counterexample in the simplest regime.
The key step
The challenge is to create a polynomial-scale gap; a constant factor does not count. Familiar even cycles are not enough. Forbidding both four-cycles and six-cycles gives exactly the same order of growth as forbidding six-cycles alone. Coning or subdividing older forest counterexamples introduces a shared dense substructure, making both sides dense at once.
The decisive move is to change the setting and use a geometric generalized quadrangle as the host graph. An ordinary projective plane also remembers the characteristic of the underlying field, but it contains six-cycles and has the wrong number of edges. A generalized quadrangle preserves the characteristic distinction, raises the shortest cycle to length eight, and lands at exactly n to the 4/3 edges. Thresholds are then placed on both sides of the bipartite graph so that they interact across the partition.
Both conjectures rest on the same intuition: simpler, sparser structures permit fewer handshakes, and the reduction follows a regular law. The two counterexamples show that this intuition fails somewhere. They are Problems 180 and 146 in the Erdős Problems database; the latter carries a $500 prize.
Multicolor Ramsey numbers
Erdős Problem 183, $250 prizeReturn to the handshake-counting party. This time, assign one of k colors to every pair of people. Once the party is large enough, there must be three people whose three pairwise connections all have exactly the same color. There is no way around it. The smallest number of people that guarantees such a triangle is the multicolor Ramsey number R(3;k).
With two colors, the answer is 6: at any party of six, there must be three mutual acquaintances or three mutual strangers. This is the famous "theorem on friends and strangers." With three colors, the number jumps to 17. With four colors, humanity still knows only that the answer lies between 51 and 62.
Erdős asked how quickly the number grows as the number of colors becomes large, and offered $100 for a proof that the limit of the kth root of R(3;k) is finite. The new superexponential lower bound answers the question: the limit is not finite. Combined with the long-known factorial upper bound, it pins the growth rate at k to the Θ(k).
The key step
Every earlier construction followed the same recipe: find a good small example, then take its product again and again. That approach has an inherent ceiling. Each product increases the number of colors and vertices in a fixed proportion, leaving the "base" that controls the growth rate unchanged. As long as the method keeps taking products, the limit must remain finite. To make it diverge, the construction needs a family whose base grows with the number of colors.
Two plausible shortcuts were ruled out. Coloring permutations by the "first displaced symbol" creates exactly the monochromatic triangle one is trying to avoid, because three permutations can move the same symbol into three different positions. Cayley graph colorings reduce to another equally difficult open problem.
The final method divides the colors into many disjoint palettes. Each block is colored internally, while edges between blocks are coordinated by a recursive rule. As the number of colors grows, the base grows with it.
Previous lower bounds were only exponential. The result also implies that graphs with independence number 2 have unbounded Shannon capacity.
What the 10 results reveal about the model
What can we infer when the 10 results are viewed together? Every point below follows from evidence already described, not from vague capability language.
1. It spans eight largely unrelated fields
These eight fields share almost no technical machinery. A Fourier method that works for sphere packing cannot simply be transferred to group von Neumann algebras. Producing results in eight areas with one model is fundamentally different from going deep enough to solve one problem in a single field.
2. It can make two kinds of move—including constructing objects
Improving an existing bound has a visible path: the target function is already there, waiting to be optimized. A counterexample must first be imagined as a structure that has never existed, then proved to satisfy several competing conditions. The non-sofic group, the family refuting Connes' rigidity conjecture, and the two extremal graph theory counterexamples all belong to this second kind. Four of the 10 results do.
3. On sphere packing, it knows when its method is exhausted
The sphere-packing result does more than improve the upper bound to 0.6044. It supplies a matching lower bound proving that no auxiliary function in the Cohn–Elkies framework can go further. In effect, the model draws the boundary of the method it just used: further progress requires a different tool.
4. The model wrote 470,000 lines of Lean itself
Once the arguments took shape, humans worked with the same model to turn them into manuscripts. The model then formalized every argument in Lean. Translating dozens of pages of mathematics into rigorous code that a machine can check line by line is a separate, extremely laborious engineering project.
5. The process included many dead ends
The 62-page reasoning walkthrough released with the results contains section titles that openly document failures: "Why the first binary recurrence was wrong," "Why the natural reduction and rooted-tree idea got stuck," and even "There is a second, more stubborn temptation." This was not a one-shot generation. It involved sustained trial, error, and reworking.
6. The inference cost is no longer a barrier
The $2,000 figure covers only tokens used to search for the answers. It excludes model training, failed attempts, and the human time later spent preparing the manuscripts. It shows that the inference stage is already inexpensive—not that "$2,000 buys 10 theorems."
Why take this seriously? Machines checked all 470,000 lines
Claims that AI has produced mathematical results are no longer novel. The dispute usually stops at the same place: who will review the work, and can anyone finish? This time, the logic check was delegated to machines. All 10 proofs were rewritten in Lean, checked line by line, and released as open-source code.
Lean is a proof assistant. A mathematical proof is rewritten in Lean's language, then a small kernel checks every line: does each step follow rigorously from earlier steps and the permitted axioms? Passing this check means the formal proof contains no logical gap.
Think of it as an auditor checking a ledger. The auditor does not need to understand your business; they verify that every entry adds up and has supporting documentation. If the numbers do not reconcile, the ledger is rejected no matter how commercially plausible the transaction seems. Lean works similarly. It does not understand what a von Neumann algebra "means"; it checks whether every inference is valid. Mathematical proofs have traditionally required experts to read them line by line, yet only a handful of people can follow all 10 fields. That review bottleneck has always haunted claims about "AI doing mathematics."
The scope of formal verification. Diagram drawn by this site from the repository structure.
We cloned the repository and counted. What does 470,000 lines mean? At one line per second, reading nonstop without food or sleep would take five and a half days. Here are our measurements:
sorry is a placeholder in Lean meaning, "skip this step for now." A single occurrence leaves a hole in the proof. There are none anywhere in the repository.
An axiom is a starting assumption at the foundation of the reasoning system, one that is not itself proved. Standard Lean uses only three: propext, Classical.choice, and Quot.sound. Secretly adding a fourth would change the rules midway through the game and invalidate the claim. These 10 proofs use only the standard three, and each result's verification configuration explicitly lists the permitted axioms.
The repository also includes an independent verification path: Comparator with nanoda. nanoda is a separate type checker implemented outside Lean's official kernel. In other words, you do not even have to trust Lean itself; you can run the proofs through an independently implemented kernel.
Lean lines in each proof (measured by this site)
Line count does not measure the importance of a result. It reflects how cumbersome the argument is to translate into machine language. The multicolor Ramsey result is powerful, yet its formalization takes only 3,000 lines.
Two ends machines cannot verify—and an open fight over authorship
Machines can guarantee only the middle of the chain. Both ends remain open.
Dark = the two completed stages
The front end: machines cannot tell whether the translation is faithful
A conjecture described in natural language for decades must first be translated into a formal Lean statement. A human or AI performs that step. If the statement is quietly weakened or a definition drifts during translation, Lean will still give it a green light. Lean checks the path from the formal statement to the conclusion; it does not decide whether the statement matches the problem mathematicians had in mind.
OpenAI prepared for scrutiny here. Under the repository's ComparatorChallenges directory, each result lists the exact theorem names to verify. The Ramsey configuration, for example, includes four statements such as ErdosProblems.MulticolourTriangleRamsey.erdos_183. This exposes the claim—"this is the theorem we say we proved"—for public inspection. Making something inspectable and having someone inspect it are not the same thing.
The back end: the review status says "agent-reviewed"
At the end of formalization.yaml in the repository root is a line the announcement does not mention:
formalization.yaml · end of file
review: status: "agent-reviewed"
In other words, the formalization's review status is agent-reviewed: reviewed by AI, not by humans. Add the fact that the 249-page paper has not been peer-reviewed and lists only "OpenAI" as its author, without a single human name, and the last box in the chain is still empty.
The published "reasoning process" is not the chain of thought
The announcement says that a narrative of the model's reasoning process was published for each solution. That can easily be mistaken for the raw chain of thought. The 62-page document explains its provenance in its own abstract: the notes were written by an AI model that read the original chain of thought and the final paper, then reconstructed how the proof came together. Anyone trying to study how the model actually reasoned is still looking through an additional layer.
The biggest disagreement is over authorship
No editorial judgment is needed here. The two documents speak clearly enough when placed side by side.
OpenAI's announcement
"We believe authorship should honestly reflect how a result was produced: describing a proof generated entirely by an AI system as human-authored would misrepresent both the system's contribution and the nature of genuine human intellectual work. We helped prepare the manuscripts, formalized the proofs in Lean, and take responsibility for their correctness, but the mathematical arguments themselves were generated by our systems."
Leiden Declaration · Endorsed by the International Mathematical Union
"When automated technology is used in published mathematical research, responsibility for the correctness and adequacy of the arguments and results... lies entirely with the human authors. Credit and responsibility remain with the human mathematical community and should not be assigned to automated systems. AI may obscure, but does not replace, the collective human labor behind a result."
In the same announcement, OpenAI says it has "deep respect and understanding" for the declaration's signatories. The declaration's values section also says that results should be attributable to identifiable authors who receive credit for the discovery and assume responsibility for its correctness. The author field of this 249-page paper contains no human names.
To be fair, OpenAI did follow another recommendation in the declaration: disclose tool use. It laid out the model, cost, and formalization process.
The database maintainer has weighed in, but the entries remain OPEN
The Erdős Problems database, erdosproblems.com, is maintained by University of Manchester mathematician Thomas Bloom. It is the field's de facto authoritative index, and OpenAI's own 249-page paper cites it.
Bloom responded on X the day of the announcement:
Big news! (Not really my area, but yes, I would rank it above the unit-distance counterexample. Maybe not above actually proving the unit-distance conjecture, but as a construction, this is a big deal.)
Thomas Bloom · X · 2026-08-01
By the "unit-distance counterexample," Bloom meant OpenAI's May result, in which another unreleased model overturned Erdős' unit-distance conjecture. He ranked these 10 results above that one "as a construction"—the kind of work described in this article's third category, where a new object must be created from scratch.
Ten minutes later, he posted again to push back against claims that this amounted to AI replacing mathematicians:
Taking a conjecture posed by a mathematician, using theory developed by mathematicians over more than a century, and proving it with an AI built by mathematicians and trained on everything mathematicians have written is not "replacing mathematicians."
Thomas Bloom · X · 2026-08-01
But his praise has not yet changed the database. When we checked the three problems again on August 2, 2026:
Multicolor Ramsey numbers
$250 prize
Degeneracy conjecture
$500 prize
Compactness conjecture
OPENAll three entries were still marked unsolved, and each said that no claimed solution, partial or complete, appeared in the comments.
These are separate facts. A maintainer's public assessment and the database's problem-by-problem verification process are not the same thing. Bloom himself noted that the work was "not really my area." He was offering a senior mathematician's assessment of its significance, not validating every step. Proper verification requires experts to read dozens of pages, inspect the statements embedded in tens of thousands of Lean lines, and confirm that those formal statements match the original problems. That takes much longer than a few days.
An authoritative figure in the field has publicly endorsed the importance of the work, while none of the 10 results has completed independent verification.
The harder tier remains out of reach—and a government review comes first
Where does this go next? Three important clues do not appear in the announcement.
They tried harder problems and failed
Noam Brown added something on the day of the announcement that the announcement itself omitted:
Yes, we did try other major problems and did not succeed. Unfortunately, no Millennium Prize Problems yet.
Noam Brown · X · 2026-08-01
But we also did not spend much compute on each problem. There is still a lot of room to scale compute during testing.
The Millennium Prize Problems are seven questions established by the Clay Mathematics Institute in 2000, each carrying a $1 million prize. After 26 years, only one has been solved.
Read together with the $2,000 figure, Brown's remarks imply this: the model solved these 10 without applying much compute. Whether scaling up can reach the highest tier remains unknown. He called Astra "a major step forward for scientific reasoning."
It may be the first model reviewed by the U.S. government
According to The Information, Astra is already being tested and is expected to be among the first models reviewed under a new U.S. government AI framework. Under that framework, models must be submitted to the federal government before public release. The framework itself is still being finalized.
For readers, the timing matters: these 10 math results are both a capability demonstration and a publication arriving just as the model approaches official review. We make no claim about motive; we are simply placing the events on the same timeline.
The longer-term goal: AI that conducts research by itself
The reporting gives two dates. OpenAI hopes to build a fully automated AI researcher capable of independently running research projects by March 2028. The nearer milestone is September this year, when it plans to produce a system operating at the level of a "research intern" to accelerate human scientists.
These 10 math results are the only tangible output produced on that roadmap so far. They show that in a field where machines can check the logic end to end, the system can already produce genuine results. They do not show whether the same approach works in fields that cannot be formally verified—which describes most scientific research.
The links and commands you need
You do not have to take either side's word in the authorship debate; all the material is public. But the announcement itself includes no links at all to the 249-page paper or the 62-page reasoning walkthrough. They can be found only through the GitHub repository's README.
After installing elan, run from the repository root
lake exe cache get lake bBuild All # 只验其中一个（球堆积），走第三方内核 lake exe comparator ComparatorChallenges/A_SpherePacking.json
An unreleased model solved 10 decades-old math problems—and machines checked every line of proof
OpenAI has presented 10 results in mathematics and theoretical computer science, publishing the paper, proof code, and cost. This illustrated one-pager explains what the results are, why they deserve attention, and what remains unverified.
↓ One-page read · Includes one animated chart
OpenAI published an announcement and a 249-page paper claiming that an internal version of its next flagship model had solved 10 long-standing problems in mathematics and theoretical computer science. The oldest was posed in 1961, and even the newest had remained open for more than 20 years. They span eight largely unrelated fields.
The model is called Astra, but it has not been released. The name never appears in the announcement itself; OpenAI researcher Noam Brown identified it on X that day.
The years when the problems behind the 10 results were posed. The axis has 11 points because the extremal graph theory result covers two conjectures. Dates come from the chapter introductions in the 249-page paper and the Erdős Problems database, checked individually by this site.
The 10 results do not all involve the same mathematical move. Splitting them into three groups shows where the model's strengths lie.
The right side of each row lists the problems in that category. The third has traditionally been the hardest to teach machines. The first two advance along a line that already exists; the third must first create a structure no one has seen, then prove that it satisfies several competing conditions. The other half of the story is breadth: the eight fields share almost no tools. A method that works for sphere packing is useless in group theory.
AI has claimed mathematical results before. The dispute always reaches the same bottleneck: who will review them, and can anyone finish? This time, the logic check went to machines.
Lean is a proof assistant. Rewrite a proof in its language, and a small kernel checks line by line whether every step follows rigorously from earlier steps and permitted axioms. Think of it as an auditor: it does not need to understand the business, only whether every ledger entry reconciles. All 10 proofs were rewritten in Lean, checked line by line, and released as open-source code.
sorry is a Lean placeholder meaning "skip this step for now"; one occurrence would leave a hole in the proof. Axioms are the unproved starting points at the foundation of the system, and adding one secretly would change the rules midway through the game. The repository also includes a separate verification path: you can distrust Lean's own kernel and rerun the proofs through an independently written one.
Machines guarantee only the middle of the chain. Both ends remain open.
A conjecture described in natural language for decades must be translated into a formal Lean statement that a machine can check line by line. A human or AI performs that step. If the statement is quietly weakened or a definition drifts during translation, Lean will still give it a green light. It checks only the path from the formal statement to the conclusion.
agent-reviewed, meaning AI reviewed this stage. As of August 2, Erdős Problems #183 / #146 / #180 were still marked unsolved in the field's de facto authoritative database, according to our direct check. Three days is far too little time for experts to inspect tens of thousands of Lean lines. This means independent verification is incomplete, even though database maintainer Thomas Bloom publicly endorsed the importance of the 10 results on X that day.Once machines handle the logic check, the argument shifts to another question: whose names belong on the proofs?
"Responsibility for the correctness and adequacy of arguments and results lies entirely with human authors. Credit and responsibility remain with the human mathematical community and should not be assigned to automated systems."
"Describing a proof generated entirely by an AI system as human-authored would misrepresent both the system's contribution and the nature of genuine human intellectual work."
The 249-page paper therefore lists only "OpenAI," with no human names.
OpenAI did follow another recommendation in the declaration: disclose tool use. The model, cost, and formalization process are all documented.
Untouched for decades?
and a 249-page paper:
an unreleased model
solved 10 old math problems.
that stood
for decades
can actually
be computed
Then prove it really works.
Can they finish?
rewrite the proof in its language, and a small program verifies
that every step follows from the ones before it.
checked line by line and open-sourced.
five and a half days
must be formalized in Lean
by a human or AI.
If the statement gets weakened,
Lean still gives a green light.
- × No one has checked the translation
- × No peer review for the 249-page paper
- × Only OpenAI appears as author
- × The review status says AI-reviewed
with the human mathematical community,
not automated systems."
human-authored would misrepresent
both the system's contribution
and genuine human work."
The two ends remain open.
Three commands let you rerun them.