In 2026, an internal version of OpenAI’s Astra model resolved or pushed forward ten long-standing problems in mathematics and theoretical computer science, and every argument was formalised into a machine-checkable Lean proof.
proved disproved interactive
Why you can trust any of this
00The setup
The headline is easy to misread. The claim is not “a chatbot said some maths”. The arguments were generated by the model (the tokens to find all ten cost roughly $2,000 at API rates), written up into papers by humans working with the same model, and then formalised in Lean, a proof assistant that checks every logical step by machine. A Lean certificate does not care who wrote the proof. It either compiles or it does not.
That last step is what makes this story different from every earlier “AI does maths” headline, so start here: this is what a proof checker does.
Claim: there are infinitely many primes (Euclid).
check it clean, then insert the flaw (a mistake humans actually make with this proof) and check again.
Each of the ten results below ships with a certificate like that, plus a released narration of how the model found the argument, including its dead ends. The chips on each section tell you which kind of result it is: PROVED means a new theorem or bound now stands, DISPROVED means a famous conjecture is dead.
Sphere packing
01High-dimensional geometry New bound
How much of space can you fill with identical balls that don’t overlap? In 2D the answer is the honeycomb, about 91%. In high dimension d nobody knows, but everything collapses exponentially: the best packings anyone can build fill about 1 part in 2d of space.
Since 1978, the strongest tool for proving upper limits was a Fourier-analytic trick (the Cohn–Elkies linear program), the same machinery behind the famous dimension-8 and dimension-24 solutions. Astra determined this tool’s exact strength: densities above 2−0.6044d are impossible, improving the 1978 exponent of 0.599 and proving this is the very best the method can do.
Densities are written as 2−c·d. Smaller c means denser. The pale zone was ruled out in 1978; the dark red strip is the newly impossible territory, and the proof shows no function-based argument of this kind can push further right.
Error-correcting codes
02Information theory New bound
A binary code is a set of bit-strings kept far apart so that a few flipped bits can’t turn one codeword into another. The core question of coding theory: how many codewords fit at a given minimum distance? The best upper bound, MRRW, dates from 1977 and had not been beaten in the exponent since.
Tap corners to pick codewords. The rule: every pair must differ in at least 2 bits (graph distance 2 on the cube). Adjacent picks turn red. Best possible here is 4.
find all 4. Hint: count the ones in each string.
Astra’s construction attaches a moving high-dimensional “harmonic space” to each codeword where the classical proof used a single fixed direction, recovering exponentially many degrees of freedom the 1977 argument threw away. Result: exponentially improved upper bounds at every distance, for binary codes and for codes on high-dimensional spheres, after nearly fifty years of no progress.
A group that can’t be simulated
03Group theory Existence proved
A group is sofic if its multiplication can be imitated, to any accuracy you like, by shuffling a large finite deck. Whether every group is sofic was a central open question, because an enormous amount of theory (“sofic implies X”) hangs off the definition. Here is the trick working perfectly on the simplest infinite group, the integers.
"Adding 1" becomes "rotate the ring". It's perfect everywhere except the seam, where the count wraps around: one error in N. Grow N and the error vanishes, so the integers are sofic.
Astra constructed a finitely presented group where no deck of any size gets below a fixed error, the first non-sofic group ever exhibited. The build is wild: a self-similar algebra where a matrix ring equals a 2×2 matrix ring over itself, a rigidity property called (T) that forces approximations into expander graphs, and Thompson’s group V, an infinite simple group, hiding inside as the poison pill no finite simulation can swallow.
The carry that broke a conjecture
04Operator algebras Disproved
Every group casts a “shadow” into analysis: its von Neumann algebra, roughly the set of all measurements you can make on the group’s natural noise. Connes conjectured in 1980 that for the most rigid groups (ICC with property (T)), the shadow determines the group: same algebra, same group. Astra found two different groups with identical shadows, and the entire difference is a primary-school idea: the carry bit.
Two-bit numbers under two laws. Law A is bitwise XOR: look at the diagonal, x+x is always 00, so nothing has order more than 2. Law B carries: 01+01 = 10, so the element 01 has order 4. Same underlying set, genuinely different groups.
The construction scales this up: two infinite groups built on the exact same coordinates and probability measure, one adding with carries and one without. Every measurement, and therefore the whole algebra, is identical; the torsion is not. The shadow cannot remember the group. Astra then shifted where the carry starts to produce infinitely many different groups sharing one algebra, answering a follow-up question of Popa’s for free.
The permanent
05Computational complexity New bound
Take a square grid of numbers. The determinant and the permanent are built from the exact same products, one per permutation. The only difference: the determinant flips half the signs, the permanent doesn’t. Yet the determinant is easy to compute and the permanent is believed to be brutally hard. Proving that hardness is one of the deepest problems in computer science.
Tap a term to light up the three cells it uses: each term picks exactly one cell per row and column. The determinant's minus signs create cancellations that clever algorithms exploit; the permanent has nowhere to hide.
Astra proved the strongest unconditional limits yet for computing it exactly: any division-free circuit needs Ω(n² log log n) operations, and any formula (a circuit that can’t reuse work) needs about n⁴/log n, up from the ~n³ known before. The proofs also show exactly why the same arguments fail for the determinant, which is the point.
Quantum games
06Quantum information Theorem proved
Two players who can’t communicate share a quantum state and face a referee’s test they win with probability at most 90%. Now the referee runs n tests in parallel. Surely the chance of sweeping all n decays exponentially? For classical players, that’s the celebrated parallel repetition theorem. For entangled players it stayed open for decades, because entanglement lets them correlate their answers across rounds in ways nothing classical can.
Entangled players can genuinely beat independent play, so the amber curve is not the truth. The theorem's contribution is the green one: however cleverly they correlate, the win probability still dies exponentially, for every finite game, with no extra assumptions.
The proof had to dodge a genuinely quantum obstacle: conditioning on winning a few rounds warps the players’ shared state by a phase that classical arguments can’t see. The fix, a “resolvent purification” that spreads each measurement across scales while preserving its probabilities exactly, is new machinery that people expect to be reused.
The closest vector
07Lattices & cryptography Hardness proved
A lattice is an endless grid of points generated by a few arrows. The closest vector problem (CVP): given any target location, find the nearest grid point. In 2D it looks like a toy. In hundreds of dimensions it is so hard that post-quantum cryptography, the encryption now shipping in your browser, bets on it.
Tap the plane.
Easy here, because you can see all the points. An algorithm only gets the arrows. With a skewed basis (toggle it) the same lattice becomes coordinates in which "nearby" is genuinely hard to find, and in high dimension there is no picture to rescue you.
It was known that CVP is NP-hard to approximate within slowly growing factors. Astra proved it stays NP-hard even within a polynomial factor n1/400, a qualitative jump made by encoding logic puzzles into lattices through finite-field algebra (Reed–Solomon codes, Hankel matrices) rather than the usual combinatorial gadgets. Good news for cryptography: the problem it leans on is even harder than certified before.
One lattice point inside
08Geometry of numbers Resolved
Ehrhart’s 1979 conjecture: take any convex shape whose centre of mass sits on a grid point, and which contains no other grid point in its interior. How big can it be? The conjectured maximum, (n+1)ⁿ/n! in dimension n, is achieved by one specific tilted simplex. In 2D that’s area 4.5. Try to beat it.
Green dot: the centroid grid point. Red dots: forbidden extra interior points. The square tops out at area 4, the disk at π, and the odd-looking simplex reaches exactly 4.5 = 3²/2!, the conjectured ceiling.
max out each shape just before a red dot appears.
Astra proved the ceiling in every dimension, and the route is the surprise: the convex body is converted into a curvature equation (Monge–Ampère), the single interior grid point becomes a one-dimensional space of holomorphic functions, and a positivity theorem from complex geometry closes a convexity gap that resisted every direct attack. A 46-year-old discrete problem, settled with complex analysis.
Ramsey numbers
09Combinatorics Resolved · Erdős #183
Colour every edge between n points with k colours. A “monochromatic triangle” is three points whose three connecting edges all got the same colour. Ramsey theory’s founding fact: with enough points, you cannot avoid one. With 2 colours the breaking point is exactly 6 points. Feel it:
Tap edges to cycle grey → red → blue. On 5 points a safe colouring exists (pentagon one colour, star the other). On 6, it provably doesn't: colour everything and a bold triangle will appear.
The open question, Erdős problem #183: as the number of colours k grows, does the breaking point Rk(3) grow like a fixed constant to the power k, or faster? Erdős offered $250 for an answer. Astra proved it grows superexponentially: Rk(3) = kΘ(k), via a recursive colouring scheme borrowed, of all places, from hat-guessing puzzles, which lets colours be reused across scales almost for free.
Forbidden graphs
10Extremal graph theory Two conjectures down
Extremal graph theory asks: if a network must avoid some forbidden pattern, how many connections can it have? A conjecture of Erdős and Simonovits (“compactness”) said that avoiding a whole family of patterns is never much harder than avoiding its single hardest member. Here is the classic warm-up showing why that’s suspicious:
On 8 points: banning 2-edge paths still allows a 4-edge matching, banning two separate edges still allows a 7-edge star, but banning both leaves a single edge. Each rule alone is cheap; together they are crushing.
That toy uses trees, which the conjecture’s serious version excludes. Astra built the real thing: a finite family of cyclic bipartite graphs, cooked from finite geometries over different number systems, where the family forces at most ~n21/16 edges while every individual member allows n4/3, a polynomial gap of n1/48. Compactness: disproved (Erdős #180). A second construction, a giant layered graph embedded in a thinned Hamming cube, killed a related degeneracy conjecture too (Erdős #146), beating its predicted n3/2 ceiling by a fixed power via an entropy argument.
Ten problems, ten different fields, one system, and every proof compiles.
The part worth arguing about
∞What it means
OpenAI’s own framing is careful in ways worth copying. They credit the mathematical arguments to the system, credit the write-ups and Lean formalisation to humans working with it, and take responsibility for correctness. They acknowledge the mathematicians, including signatories of the Leiden declaration, who are uneasy about what this does to the discipline. And an earlier result from the same effort (a disproof of an Erdős unit-distance conjecture) has already seeded a list of follow-up papers by human mathematicians, which is the healthiest possible sign: the results are becoming raw material, not trophies.
Two things can be true at once. Mathematics just gained an instrument, the way astronomy once gained the telescope. And the community, not the instrument’s maker, will decide what looking through it should mean.
Further reading
- ”Ten Advances in Mathematics and Theoretical Computer Science”, the paper (PDF)
- The reasoning walkthroughs behind each result (PDF)
- Erdős problem #183, multicolour Ramsey numbers
- Erdős problem #180, the compactness conjecture
- Erdős problem #146, the degeneracy conjecture
- Lean, the proof assistant behind the certificates
Every demo on this page is a simulation with hand-picked data: no theorem provers or models run in your browser. The demos teach the shape of each problem; the proofs live in the paper and its Lean certificates. Numbers quoted (exponents, bounds, costs) come from the paper and the published walkthroughs.