Astra and the Group That Broke the Rules

Every few months, an AI lab announces something and the announcement contains the word "breakthrough" so many times that you develop a protective callus and stop reading. This week's news deserves better treatment than that, because underneath the inevitable press-release gloss sits a genuinely odd little fact: a group of mathematicians spent twenty-seven years failing to answer a question, and a language model answered it over what was presumably a fairly ordinary Tuesday, for about the cost of a decent office chair.

OpenAI says an internal, unreleased version of its next model, codenamed Astra, has produced new results on ten long-standing open problems in mathematics and theoretical computer science, each of which had been sitting unsolved for at least a decade. The company published a 249-page manuscript collection alongside machine-checkable Lean 4 proof certificates on GitHub, under an Apache 2.0 licence, for anyone who fancies an evening of verifying group theory. Total compute cost for the lot: approximately $2,000. For context, that is less than what most mid-sized companies spend on the coffee machine in their all-hands meeting room.

 

The Headline Result: A Group That Refuses to Behave

The result getting the most attention, and reasonably so, concerns something called sofic groups, which is one of those pieces of mathematics that sounds like a made-up word until you learn that Mikhail Gromov coined the concept in 1999 and mathematicians have been quietly obsessing over it ever since. A group is "sofic" if its behaviour can be approximated, arbitrarily closely, by finite permutation systems: essentially, can you fake this infinite structure well enough using only finite pieces that no one downstream can tell the difference. Every group mathematicians actually use day to day, amenable groups, residually finite groups, the whole practical toolkit, turns out to be sofic. The open question, for twenty-seven years, was whether every countable discrete group has to be. Whether soficity was, in effect, compulsory.

Astra constructed the first known counterexample. A non-sofic group. A structure that exists, follows all the rules of group theory, and simply refuses to be approximated the way its well-behaved cousins are. If that sounds abstract, it's because it is, deliberately, the kind of abstract that makes a career. Gromov asked the question in 1999 and the field has been chewing on it since before most of the developers reading this were writing their first for-loop.

 

And the Other Nine, Briefly, Because They're Also Not Nothing

The non-sofic group is the one making headlines, but the supporting cast is unusually strong for a supporting cast. Astra disproved Connes's rigidity conjecture on von Neumann algebras, proved Ehrhart's volume conjecture, resolved three problems from Paul Erdos's famous open-problems catalogue, including problem 183 on multicoloured Ramsey numbers, produced the first improvement to the general upper bound on high-dimensional sphere-packing density since 1978 (a field where "improvement" is measured in decimal places that took human mathematicians careers to shave off), proved a parallel repetition theorem for two-player quantum games, and established new lower bounds on the circuit complexity of computing the permanent. Any one of these, published by a postdoc, would make that postdoc's decade. Astra produced all ten in what one imagines was, from the model's perspective, a fairly unremarkable batch job.

 

 

The Eyebrow That Stays Raised

None of which means the mathematics establishment has issued a group hug. The results have been reviewed informally by mathematicians who saw preprints and, by most accounts, came away impressed, but none of the ten has yet gone through a formal, refereed journal process. That distinction matters more in mathematics than almost anywhere else in science, because peer review in this field isn't a rubber stamp exercise, it's the profession's actual mechanism for catching the subtle sort of error where a definition has been quietly stretched three sentences before the theorem that needs it. Lean verification tells you the logic is internally consistent given its premises. It does not, by itself, tell you the premises are the ones the field actually cares about, or that the proof strategy generalises usefully, or that "non-sofic group" as constructed here is the counterexample mathematicians will actually want to build on rather than a curious edge case. That verdict takes longer than a press cycle, and rightly so.

There's also the small matter that this is an unreleased, internal model. We are being told about Astra's capabilities by the people who benefit most from us being impressed by them, which isn't an accusation, it's just how the incentive structure works, and it's worth remembering every time a lab announces something using its own model, on its own terms, ahead of its own commercial release. The Lean certificates are independently checkable. The claim that this represents Astra's typical performance, rather than its most photogenic outing, is not.

 

Why This Matters More Than the Usual Benchmark Chatter

I've written before, on this blog, about being fairly unimpressed by leaderboard chasing: the monthly ritual where one frontier model edges out another by two percentage points on a benchmark that increasingly resembles the test rather than the skill it was meant to measure. This is a different category of thing entirely. Solving an open problem isn't a benchmark, because there was no benchmark to game, no held-out answer key, no training data leakage to squint at suspiciously. Gromov's question didn't have an answer sitting in a dataset somewhere waiting to be memorised. It had no answer at all, for twenty-seven years, until it had one.

That is the thing worth sitting with. Not "AI is good at maths now," which is a headline that has been technically true and practically overstated for a couple of years. The more precise claim is: a system generated genuinely new mathematical knowledge, in a form rigorous enough to check mechanically rather than take on trust, at a cost that makes "we didn't have the budget for this line of research" sound like an excuse from an earlier decade. Whether Astra's next ten attempts land with the same success rate, whether the field absorbs these results as real contributions or interesting curiosities, and whether $2,000 buys you one non-sofic group or a hundred failed attempts and one lucky one, we genuinely don't know yet. But the direction of travel is unmistakable, and it's aimed somewhere mathematicians used to assume only humans, working very slowly, over very long careers, were allowed to go.

All Posts