DEV Community

Cover image for The Summer Math Fell to the Machines
Nsoro Allan
Nsoro Allan

Posted on

The Summer Math Fell to the Machines

“AI has killed more open math problems in the last few weeks than the entire human race managed in the previous decade.”

  • Fireship, August 2026

Yeah… that one hit different.

For most of us who write code for a living, math has always felt like this distant, slightly intimidating cousin. We use it, we respect it, but we don’t usually lose sleep over century-old conjectures. Then this summer happened. In the span of a few weeks, several long-standing open problems simply… fell. Some during the World Cup final. One after four short prompts. Another batch arrived with formal Lean proofs you can check yourself on GitHub.

It feels less like incremental progress and more like the ground shifting under one of humanity’s oldest intellectual games.

The body count (a very short summer)

First up: the Jacobian conjecture. Keller posed it in 1939. It sat on Smale’s famous list of problems for the 21st century. Generations of mathematicians tried to prove it true. In July 2026, Levent Alpöge (with help from Anthropic’s Claude Fable 5) posted a short, explicit counterexample in three variables. The map has a constant non-zero Jacobian determinant yet isn’t invertible. Anyone with a computer algebra system can verify it in minutes. The general case (for dimension greater than 2) is now false. The classic two-variable version is still open, but the main conjecture is settled and it only took a few hours of human-AI collaboration during a football match.

A few days later came the Dinitz–Garg–Goemans conjecture, a roughly 30-year-old question in combinatorial optimization about unsplittable flows. Dmitry Rybin fed GPT-5.6 Pro four short prompts (under 60 words total). A few hours later he had a counterexample: a small graph where the fractional cost is 58 but every qualifying unsplittable flow costs at least 60. The arithmetic is straightforward to check.

Then OpenAI dropped its Astra results. An internal version of their next major model produced ten new results across mathematics and theoretical computer science problems that had seen no real progress on the main claim for at least a decade. They published a long manuscript, reasoning walkthroughs, and, most importantly, Lean 4 certificates on GitHub. You can clone the repo and let the proof assistant check every step. Highlights include the first explicit non-sofic group, a disproof of Connes’s rigidity conjecture, better high-dimensional sphere-packing bounds, and several Erdős problems. The reported search cost for all ten was around two thousand dollars at API rates.

And that wasn’t even the first shot of the year. Back in May an OpenAI model had already produced a counterexample to the Erdős unit-distance problem from 1946. The pattern is hard to ignore.

How this is actually working

It’s not magic, and it’s not pure “the AI just knew.” The current recipe looks roughly like this:

Reasoning models that can hold long chains of mathematical thought and propose candidate constructions.

Test-time compute throwing more inference at the problem so the model can explore wider.

Formal verification (Lean especially). Once you have a candidate argument, you can try to formalize it so a small trusted kernel checks every logical step. A clean compile is much stronger than “the model said so.”

And, critically, human guidance. Someone still has to ask the right question, filter the nonsense, recognize when something is interesting, and decide what it means.

The Lean certificates are the part that should make developers sit up. We’re used to “AI generated this code, hope it’s fine.” Here the community is getting machine-checkable artifacts alongside the claims. That’s a different level of trust.

Why a lot of mathematicians feel unsettled

Terence Tao’s ICM 2026 talk (now an essay called “Mathematics in the age of AI”) puts it cleanly. For a long time the field lived with proof scarcity. Finding a correct argument for a hard statement was rare and precious. We’re moving into an era of proof abundance. Machines can now generate long, correct formal proofs faster than most humans can comfortably read and digest them.

That changes the game. Questions of credit get weird. Understanding starts to matter more than mere verification. The value of human insight shifts toward choosing problems, interpreting results, building conceptual frameworks, and deciding what is actually worth caring about. Tao frames it as a second crisis in the foundations of the field not of logic this time, but of values and practices. The healthy response, he suggests, is to examine those values rather than pretend the capability shift isn’t happening.

What this means for the rest of us

If you write software, the same techniques that just toppled conjectures are coming for your verification problems.

Formal methods and verified software just got a serious boost. The workflow of “generate candidates, then machine-check them” maps almost directly onto proving properties of code, protocols, compilers, and security-critical systems. The same search-plus-verification loop that finds counterexamples to old conjectures can help explore complex design spaces while a proof assistant keeps you honest.

There’s a clear opportunity here: learn a bit of Lean (or another proof assistant), treat modern reasoning models as co-pilots that can explore vast spaces while you supply direction and judgment, and start formalizing small pieces of real systems. Competition math was always a kind of easy mode. Research mathematics is now under real pressure, but the deeper work of understanding, framing new questions, and deciding what matters still needs humans. The same distinction applies to software.

Closing thought

We’re watching one of the oldest intellectual pursuits on the planet get rewritten in real time. The machines didn’t just solve a few problems. They forced the field to ask, more sharply than before, what mathematics is actually for.

The comfortable claim that “AI can’t do real math” is done. The more interesting question how humans and machines should collaborate on understanding, verification, and discovery is just getting started.

If you want to dig in:

Watch the Fireship video that captured the moment.

Read the OpenAI announcement and clone the Lean certificates.

Look at the New Scientist pieces on the Jacobian and Dinitz results.

Read Tao’s essay.

And maybe try formalizing something small yourself a short algorithm, an invariant, a toy theorem. The tools are public. The only real question left is what you’ll do with them.

References

Top comments (0)