On August 1st, an AI solved ten mathematics problems that had stumped the world’s best minds for decades. One of them had been open since 1999. The total compute cost: roughly $2,000.
I’ve been writing about AI long enough that I’ve learned to calibrate my own excitement. When a headline says “AI beats humans at X,” I read it as background noise now. Of course it does. AI beats radiologists at reading scans. It beats champions at chess, Go, and protein folding. Beating humans stopped being news about four years ago.
But something happened last week that I couldn’t write off. On August 1st, 2026, OpenAI published ten formal mathematical proofs produced by Astra, its next model family (not yet generally available, though OpenAI has disclosed the compute cost at current GPT-5.6 Sol API rates). The proofs were submitted to GitHub with machine-checkable Lean 4 certificates and a “sorry count” of zero. In mathematics, a “sorry” is a placeholder for an unproven step, a flag that says “I’ll come back to this.” Zero sorries means no fudged steps. Every single logical move was verified.
This isn’t about AI beating humans. Humans didn’t find this one.
The Problem That Sat Open for 27 Years
To understand why this matters, you need a brief detour into an area of mathematics called group theory.
In 1999, mathematician Mikhail Gromov introduced the conceptual framework that Benjamin Weiss would later formalize as “soficity.” The technical definition is dense, but the intuition is this: a sofic group is one that can be approximated by finite symmetric groups. In plain English, it’s a group that behaves, in a measurable sense, like something finite even when it’s actually infinite.
Gromov and others suspected that every group was sofic. It was a reasonable conjecture. Nobody could find a counterexample. The question sat open for 27 years as one of the central unsolved problems in group theory: does there exist a group that is not sofic?
Astra answered it. Yes. Here’s one.
The proof is 249 pages. OpenAI didn’t release a human companion paper explaining Astra’s reasoning. They released the model’s own chain-of-thought walkthroughs, Astra’s account of its own thinking, step by step. There’s no human translation of this proof. What exists is the machine’s narration of how it got there, and the Lean 4 certificates confirming every step was correct. The field can verify the result. It hasn’t yet produced its own derivation.
What $2,000 Buys You
The compute cost to find all ten proofs was roughly $2,000 at GPT-5.6 Sol API rates.
I keep coming back to that number. A Fields Medal carries a cash prize of around $15,000 Canadian dollars. The average annual salary for a research mathematician in the United States is somewhere north of $90,000. The non-sofic groups problem had been sitting unanswered since before many of today’s PhD students were born.
Two thousand dollars.
Yes, the model behind it cost billions to train. But the marginal cost of pointing an existing system at this problem was $2,000. And it’s the marginal cost that scales.
That’s less than a used car. Less than a semester of textbooks. Less than some people spend on golf clubs. And for that, Astra produced a formal, machine-verified solution to a problem that the collective intelligence of the global mathematics community could not crack in nearly three decades.
I don’t say this to diminish mathematicians. The question itself required profound human creativity to even formulate. Gromov’s 1999 framework was itself a brilliant conceptual leap. But the resolution, the closing of the gap, came from a machine that didn’t need to sleep, didn’t need tenure, and didn’t need to publish or perish.
This is the part people miss in almost every AI discussion: the interesting story isn’t “AI is faster than humans.” The interesting story is “AI is finding things humans weren’t finding at all.”
The Lean 4 Angle Nobody’s Talking About
Most coverage of the Astra results focused on the headline: AI solves 27-year-old problem. Fair enough. But the Lean 4 angle deserves more attention.
Lean 4 is a formal proof assistant. When you write a proof in Lean 4, you’re not writing an argument that sounds persuasive. You’re writing code that a machine can verify step-by-step. Every logical inference is checked. If anything slips past, the system flags it.
Traditional mathematical proofs are social objects. They’re read by humans, debated by humans, and occasionally found to contain subtle errors years later. The history of mathematics has more than a few famous “proofs” that turned out to have holes. Andrew Wiles’s first proof of Fermat’s Last Theorem had a gap. It took him another year to fix it.
Astra’s proofs have zero sorries. Zero unverified steps. If the Lean 4 framework is correct (and it is rigorously maintained), these proofs are not “probably right.” They’re verified in a way no human-written proof can claim to be.
This is a different kind of mathematical authority than we’ve ever seen before. Not consensus. Not peer review. Formal verification.
The Translation Problem
What OpenAI released alongside the Lean 4 certificates wasn’t a paper by human mathematicians explaining Astra’s work. It was the model’s own chain-of-thought walkthroughs: the machine’s account of its own reasoning.
That’s worth sitting with. For the earlier unit distance result in May, nine external mathematicians including Tim Gowers and Noga Alon wrote a companion paper so the field could follow along. For the non-sofic result (the harder one, the one open since 1999) there’s no such paper yet. There’s a 249-page manuscript from Astra, the Lean certificates, and the model’s own narration of how it got there.
Remarkable because it suggests the AI isn’t simply recombining known techniques. It found a path that humans hadn’t walked before, one that’s unfamiliar enough that the field is still working out what to make of it.
Unsettling because it raises a question we’re going to be wrestling with for decades: what happens when AI mathematics consistently produces results that humans can verify but can’t independently derive?
There’s a precedent. In physics, we’ve long relied on mathematical frameworks that outrun our physical intuition. Quantum mechanics was correct before anyone had a good mental picture of what it meant. Mathematicians learned to operate in that gap.
But that was a gap between human intuition and human-constructed mathematics. What Astra introduces is a new gap: between human derivation and machine derivation. We can check the steps. We can’t follow the leaps.
That’s a new relationship with knowledge, and I think most people aren’t ready for it.
Why This Matters Beyond Mathematics
If you’re not a mathematician, you might be asking why any of this is relevant to your life. Fair question.
The reason is that every hard problem, including problems in drug discovery, materials science, logistics, cryptography, and climate modeling, has mathematical structure underneath it. The techniques Astra used to close the non-sofic groups question are not the same techniques that will find the next class of antibiotics. But the capability they represent, the ability to explore formal mathematical space at low cost and produce machine-verified results, is going to be redirected at every domain where the hard part is proving something true.
Two thousand dollars closed a 27-year gap in abstract algebra. The same class of system, running on more compute and pointed at protein binding sites or quantum error correction codes, is going to do things we haven’t imagined yet.
Thomas Bloom, who maintains the Erdős problem catalogue, called the August results “big news” and noted they were even more significant than the unit distance breakthrough earlier in the year. Bloom has been tracking open problems across mathematics for years. He’s not easily impressed.
When the people who track what’s unsolved start calling something big news, it’s worth paying attention.
The Milestone That Didn’t Feel Like One
Here’s my honest take: I think most people are going to process the Astra announcement wrong.
The framing will be “AI is getting smarter.” That’s true, but it misses the point. The frame that matters is “the set of problems accessible to humanity just expanded, and the price of entry dropped to $2,000.”
We’ve had mathematical software for decades. Wolfram Alpha, Mathematica, various proof assistants. They’re tools. You still needed a human expert to know which problem to point them at, which approach to try, which dead ends to abandon. The tools amplified human mathematicians.
What Astra appears to do is something different: it finds. It doesn’t just verify human conjectures, it explores the space, locates the proofs, and returns the certificates. The human’s job shifts from “do the mathematics” to “ask the right question.”
That’s a quiet revolution. It doesn’t look dramatic from the outside. But it’s a revolution nonetheless.
The 27-year-old question has an answer now. The answer is yes: non-sofic groups exist. The proof is verified. The machine’s own account of its reasoning is the only translation that exists.
And it cost $2,000.
Chris Meredith writes about AI, technology, and what happens when the future arrives faster than the conversation about it. Follow at @ChristopherMeredith.
Chris Meredith writes about AI, technology, and what it actually means for real people. Follow along on Substack: monkeyattack.substack.com
