Four days after I published a piece arguing LLMs can't make the jump, OpenAI announced that an internal model called Astra had solved ten open problems in mathematics and theoretical computer science. One of them had been open since 1999.
I'm not going to pretend that's a comfortable coincidence to sit with. So let's sit with it properly instead of pretending it didn't happen.
The headline result is a non-sofic group. Mikhail Gromov introduced the concept of soficity in 1999 and asked whether every countable group has to be sofic. Twenty-seven years, no mathematician managed to prove or disprove it. Astra built the counterexample. The certificate ships on GitHub in Lean 4, formally verified, "sorry" count zero — meaning no step in the proof was left unproven, no trust in OpenAI required. Total inference cost for all ten results combined: about $2,000.
Thomas Bloom, who curates the Erdős problems catalogue at Manchester, called it big news. Worth knowing: Bloom is the same mathematician who publicly dismantled an earlier false OpenAI math claim last October. His endorsement here isn't a company's own press release getting nodded along. It's the field's most skeptical reader saying this one holds.
So: extraordinary, verified, real. Now the question that actually matters for the piece I wrote.
Valerio Capraro, a mathematician who did his PhD on a problem adjacent to Gromov's conjecture, posted the sharpest version of the distinction I was reaching for and didn't quite land. Astra solved difficult problems inside existing conceptual worlds. Calculus, topology, scheme theory did something different — they didn't answer questions sitting inside a framework, they built frameworks new questions could be asked in.
Non-sofic groups existing or not was always a well-posed question inside group theory as it already stood. Astra found the object. It didn't invent group theory. That's the line: solving hard problems inside a conceptual world is not the same act as inventing the world.
Worth naming plainly, because it cuts the other way against overclaiming too: even a Lean certificate that type-checks doesn't confirm the formal statement actually captures the open problem the way mathematicians understood it. Someone still has to judge whether the formalization is asking the right question. That judgment is exactly the kind of move nobody automated here.
A commenter, Seo, pushed on something I'd been sloppy about. Is "the jump" one mechanism, or several? Einstein's move was importing an outside framework — he read Hume and Mach until he had the nerve to throw out absolute simultaneity. Dirac's move was different. He wasn't handed a wrong answer. Bohr told him Klein had already solved the relativistic electron problem. Dirac went and found a different one anyway, because Klein's didn't fit what he called his darling theory.
Importing something from outside the problem, and rejecting a correct-but-unsatisfying answer on the strength of your own priors, are not obviously the same action. I don't have a clean answer for whether they reduce to one mechanism. I'd rather leave that open than force it, because forcing it is exactly the kind of premature tidiness the whole piece is arguing against.
Here's where it stops being abstract. Sean Goedecke wrote about Terence Tao's public conversation with ChatGPT on a counterexample to the Jacobian Conjecture. Tao's messages are short. The model's outputs, talking to him, are unusually concise — expertise shunts it out of explaining-to-amateurs mode. He pushes back without contradicting directly: "this looks more complex than I was hoping for." And the detail that matters most: Tao makes the leaps himself. He almost never takes the model's suggested next move.
Goedecke's conclusion: the human is the bottleneck, not the model, because the hard part is communicating exactly what kind of solution you want. The information is already in the model. It takes a very smart human to pull it out.
That's my bookmark-time argument, relocated. I've been deciding what's worth saving since 2016, one bookmark at a time, and calling that curation. Tao is doing the same thing in real time, inside a chat window, calling it prompting. Different timescale, same move: supply the frame, let the model fill it.
So the thesis needs updating, not abandoning. Not "LLMs can't jump." Something narrower and, I think, more true. Inside closed, formally verifiable worlds — math, code, games, anything with a Lean checker or a compiler or a scoreboard — the jump is getting crackable by scale and search, and Astra just proved it faster than I expected. Outside those worlds, in anything ambiguous, causally tangled, unverifiable in advance, nobody's shown it yet. Not the actual Einstein case. Not the actual geophysics case. Not the actual "is this bookmark worth keeping" case. And the people getting the most out of these models, Tao included, are the ones still doing that part themselves.
I got four days. Most theses don't get tested this fast, or this publicly. I'd rather be corrected in the open than be right by accident.
Top comments (5)
This is such an accurate way to frame Astra’s breakthrough. AI can tackle tough, clearly defined open problems inside established formal frameworks, yet it still can’t build entirely new conceptual paradigms or come up with those foundational open questions on its own. Humans are still the irreplaceable bottleneck when it comes to framing judgment and paradigm-shifting creativity.
Appreciate it, Luna and "framing judgment" is a nice compression of the whole argument. Curious whether you think that bottleneck gets narrower over time or whether it's structural regardless of scale...
My simple gut feeling (not based on any kind of knowledge or expertise, lol) says it's probably structural, and it's because current generation LLMs are "rigid" ...
What if someone would come up with a way to add "neuroplasticity" to AI/LLMs - would that be the fundamental 'game changer' they're apparently looking for ("AGI")?
At the same time, any 'fundamental' breakthrough of that kind might be incredibly risky and might open that Pandora's box which we'll then probably wish had never been opened - "be careful what you wish for" :-)
P.S. putting that more simply - if ever AI can do exactly the same things a human can do then we're screwed, it's the end - right, or not? I think that would be something we simply should not want ...
"That's the line: solving hard problems inside a conceptual world is not the same act as inventing the world." - yeah I think that's spot on, that's still the difference between what the "robot" (no matter how smart) and the human can do ...
Right nd it's a good, clean way to put the whole thing — "smart" and "can invent the world" turn out to be separate axes not degrees of the same one.