Math Was Humanity's Last Fort. It Just Got Breached — But Computer Proof Isn't New

Math was the last fortress. Chess fell in 1997. Art in 2022. Code last year. But math — the kind that needs insight, beauty, connections no one thought to make — that was still human territory.

Not anymore. An OpenAI general-purpose reasoning model has disproved Erdős’s unit distance conjecture, open since 1946¹. Fields Medalist Tim Gowers said he’d recommend it for the Annals of Mathematics “without any hesitation”². This one’s real — unlike last November when Kevin Weil’s claim that “GPT-5 solved 10 Erdős problems” turned out to be rediscoveries of existing papers, called “a dramatic misrepresentation” by Thomas Bloom (who maintains the Erdős Problems site)³. This time Bloom co-authored the companion paper².

But the story isn’t just “another field conquered by AI.” Because computer proof isn’t new.

Computer proof has been around since 1976

In 1976, Appel and Haken proved the four color theorem using a computer — any map can be colored with four colors so adjacent regions don’t clash⁴. The math community was shaken: the proof required computer enumeration of over a thousand cases, impossible for a human to verify line by line.

Many were uncomfortable. Some said it wasn’t a “real proof” because you couldn’t read it. Others said the machine was just doing what humans told it to — no mathematical insight.

They had a point. But the four color theorem still hasn’t been proven “purely by hand.” And over 50 years, the math community has accepted that computers can be proof tools. Coq, Lean, Isabelle — proof assistants are embedded in mathematical workflows⁵. Since January 2026, AI has moved 15 Erdős problems from open to solved⁶.

So the question was never “can machines prove things.” They’ve been doing that for half a century.

The question is: is the machine computing for you, or thinking for you?

What’s different this time

Erdős’s unit distance problem is simple: among n points in the plane, how many pairs can be exactly distance 1 apart?¹

Everyone assumed the answer was roughly linear. A square grid gives 2n pairs. Erdős’s own construction did slightly better — n^(1+C/log log n) — but only a hair above linear¹. The best upper bound, O(n^(4/3)), came from Spencer, Szemerédi, and Trotter in 1984⁷. 42 years, no movement.

Erdős conjectured u(n) ≤ n^(1+o(1))⁴. Everyone believed it.

Table 1: 80 years, stuck ¹⁷

Year	Result	Who
1946	Best lower bound: n^(1+C/log log n)	Erdős himself
1984	Best upper bound: O(n^(4/3))	Spencer, Szemerédi, Trotter
2026	Disproved: u(n) ≥ n^(1+δ), δ=0.014	OpenAI model + Will Sawin refinement

How did the model do it? It looked for counterexamples.

That sounds trivial, but think about what every human who attacked this problem did — they tried to prove the conjecture was true. The model’s chain of thought showed it spent most of its compute constructing counterexamples². It wasn’t trapped by “everyone believes this should be true.” It didn’t know the social consensus, so it tried the direction humans collectively ruled out.

Gowers noticed: “A significant majority of the thoughts are trying to construct a counterexample, rather than trying to prove it. This argues that the model has some combination of good intuition, willingness to try approaches considered long-shot by the community.”²

This is “vibe math” — iterative theorem development through conversation with an LLM⁵. Not “give it a proposition, get a proof.” It tries, checks, refines, tries again until it finds a path.

Algebraic number theory walks in the back door

Then comes the part nobody expected.

The model didn’t stay in combinatorial geometry. It jumped to a field that looks completely unrelated — algebraic number theory. It replaced Erdős’s Gaussian integers (a + bi) with more complex algebraic number fields, using infinite class field towers and Golod-Shafarevich theory¹².

These are standard tools within algebraic number theory. Nobody had thought to apply them to point sets in the Euclidean plane.

Table 2: Humans and AI looked through different doors ¹²

	Humans	AI
Where they searched	Combinatorial geometry	Algebraic number theory
Tools used	Combinatorial arguments	Class field towers, Golod-Shafarevich
Strategy	Prove the conjecture	Construct counterexamples
Result	Didn’t prove it	n^(1+0.014)

Princeton’s Will Sawin pinned down δ = 0.014². That looks tiny. But it’s not “slightly above linear” — it’s “a fixed polynomial advantage.” In asymptotic analysis, that’s a fundamental distinction.

Alon didn’t hedge: “The fact that the AI was able to do here what lots of excellent human researchers tried and failed to do.”²

Bloom went further: “AI is helping us to more fully explore the cathedral of mathematics we have built over the centuries; what other unseen wonders are waiting in the wings?”¹

But Gowers poured cold water — honestly.

Disproved, not proven

Gowers compared this to Guth and Katz’s 2005 proof of the Erdős distinct distances problem. That proof introduced the polynomial partition method — a genuinely new tool that opened up a whole direction and solved several subsequent problems.

This construction doesn’t do that. It’s a bridge pulled in from number theory, not a new geometric theory. It “does not introduce powerful new geometric tools, or hitherto unsuspected structural results”².

Gowers’s verdict: counterexamples can potentially be found by search. Proofs require real theory-building. “Perhaps what we are seeing at the moment is not that AI is about to overtake human mathematicians, but rather that there are certain styles of problem where it has a distinct advantage — encyclopaedic knowledge, no time management worries, and it can afford to try statements that seem unlikely to be true.”²

Translation: AI is good at searching. Not yet at building.

This tracks with the history of computer proof. The 1976 four color theorem was also a search — enumerating over a thousand configurations. Only this time, the search wasn’t across configurations. It was across domains of mathematics.

Not verified in Lean

One detail worth noting: the proof hasn’t been formally verified. No Lean, no Coq. Nine top mathematicians read it and confirmed it².

The four color theorem was eventually formalized in Coq (2005, Georges Gonthier). Many AI-generated Erdős solutions have been verified in Lean⁵. But this proof is natural language, checked by humans word by word.

Is this “computer proof”? Depends where you draw the line. If “computer proof” means “machine output confirmed by humans,” the four color theorem was one in 1976. If it means “machine independently completes the full chain from proposition to QED in a formal system,” this one doesn’t qualify yet.

But this proof did something the four color theorem didn’t: it found a path humans hadn’t found. Four color theorem: humans devised the strategy, machines executed. This time: the machine found the door to algebraic number theory on its own.

References

Conclusion

Math was the last hard thing humans had that machines hadn’t touched. That’s been breached. But look back — the four color theorem was computer-proved in 1976. Coq and Lean are already embedded in research. Computer proof isn’t new; AI solving Erdős problems isn’t new either.

What’s different: before, computers computed for you. This time, the machine searched for a path — and found one from algebraic number theory to discrete geometry that humans missed, not because it was too hard, but because “everyone believed it should be provable.”

But Gowers put it honestly: counterexamples can be found by search. Real theory-building can’t. The machine found a counterexample, not a new theory.

Over the next months, algebraic number theorists will be looking at other open problems in discrete geometry². If what’s behind that door is more counterexamples — fine, AI is a faster search engine. If what’s behind it is the kind of new theory Guth and Katz found — that’s when it gets really different.

Footnotes

1. OpenAI Official Blog — An OpenAI model has disproved a central conjecture in discrete geometry https://openai.com/index/model-disproves-discrete-geometry-conjecture/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷

2. Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Wood — Companion paper — Human-digested proof and expert commentary https://arxiv.org/abs/2605.20695 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹ ↩¹²

3. TechCrunch — “OpenAI claims it solved an 80-year-old math problem — for real this time” — Previous false claim context https://techcrunch.com/2026/05/20/openai-claims-it-solved-an-80-year-old-math-problem-for-real-this-time/ ↩

4. Gil Kalai — “Amazing: Erdős’ Unit Distance Problem was Disproved!” — Compares this to the 1976 four color theorem https://gilkalai.wordpress.com/2026/05/21/amazing-erdos-unit-distance-problem-was-disproved-it-was-achieved-by-ai/ ↩ ↩²

5. arXiv 2602.18918 — “Vibe-proving”: iterative conversational theorem development with LLMs https://arxiv.org/abs/2602.18918 ↩ ↩² ↩³

6. CryptoBriefing — 15 Erdős problems solved since January 2026, AI credited in 11 https://cryptobriefing.com/openai-ai-solves-erdos-math-conjecture/ ↩

7. Spencer, Szemerédi, Trotter (1984) — Upper bound O(n^(4/3)), unchanged for 42 years Referenced in companion paper ↩ ↩²