Why every recent AI math win starts with a counterexample

OpenAI said its latest model disproved a 1946 conjecture by Paul Erdős about how many unit-distance pairs a set of points can have. The result was a counterexample, not a proof of the conjecture itself. The model imported algebraic number-theory tools into a problem most working combinatorialists had not seen solved with them.

For Timothy Gowers, a 1998 Fields Medalist, the unit-distance result is one of a recent cluster of AI math wins that all do the same thing. In remarks published alongside the human-verified digest of the AI proof, he noted that OpenAI's win, Claude's help to Levent Alpöge on a counterexample related to the Jacobi conjecture, a constructed non-sofic group, and a multi-color Ramsey lower bound all share one structural move. Each one tries to find a single object in a large space that breaks the claim, instead of deriving the claim from axioms.

Brass, Moser, and Pach called the unit-distance problem "possibly the best known (and simplest to explain) problem in combinatorial geometry" in their 2005 book, and Noga Alon has called it one of Erdős's favorite problems. Disproving it required a construction: an infinite family of point sets with more unit-distance pairs than the conjectured ceiling. Gowers and eight other named mathematicians, including Noga Alon, Thomas F. Bloom, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood, then redigested the AI's argument into a human-readable proof. The same preprint is on arXiv.

Per a third-party X post, when given enough compute, the internal OpenAI model reportedly solves the unit-distance problem 48% of the time on a single autonomous attempt, without Lean or a human-in-the-loop wrapper. The 48% figure is third-party commentary, not an OpenAI claim, and it is the kind of number that makes Gowers' "why" question easier to see.

Gowers gives two reasons AI is unusually good at counterexample tasks. The first is cross-domain tool knowledge: the model can pull in algebraic machinery that the typical discrete geometer has not studied. The second is the low marginal cost of attempts. The Chinese outlet QbitAI pegged the cost of OpenAI's full 10-result math batch at roughly "数千美元" of API-priced tokens, a few thousand US dollars. At that price, the model can run a search tree no human would have time to walk.

Gowers is careful to distinguish AI's pattern from classical proof by contradiction. In proof by contradiction, you assume a negation and derive a contradiction inside a closed logical system. AI's move is different. It samples candidates from an enormous object space and checks which one fails. The math is the same, but the cognitive shape is search, not deduction. Each failed candidate is cheap. The win is finding the one that fails.

The limit Gowers points to is what he calls the mathematician's "nose". A working mathematician does not just try objects. They prune branches of the search tree that look unpromising, on intuition built from years of failed attempts and half-remembered analogies. AI can fill the tree but cannot decide which branches to skip. Gowers does not say this is permanent. He says it is the current shape of the boundary, and the boundary is the part worth watching.

The next test is easy to state. If the next AI math win still needs a human to pose the conjecture, Gowers' nose limit holds. If a model starts picking its own targets and pruning its own branches, the limit has moved. Right now, the unit-distance win needed Erdős to set the problem in 1946, and it needed nine named mathematicians to certify the proof in days rather than months. The pattern holds.