Human mathematicians are being outcounterexampled

Two months ago today (20th May 2026), ChatGPT disproved Erdős’ Unit Distance conjecture in discrete geometry. This is now old news but I had to start somewhere. The announcement was accompanied with testimonies by human mathematicians, many of whom I knew and a few of whom I trusted, saying that they believed the argument (they had been given early access to it and had checked it). The basic structure of the proof is that a profound theorem in number theory due to Golod and Shafarevich from the 1960s could be used to construct a counterexample to the conjecture.

With the development of the theory of finite flat group schemes back on track, I could relax back into the FLT workshop. On Tuesday 7th July I sat opposite Akhil Mathew at lunch; Akhil is a professor of mathematics at UChicago and he was an attendee who had been experimenting with the tools available. We talked about potential questions which AI could work on, and Akhil raised the old question of Grothendieck about whether every finite free group scheme of order n was killed by n. Deligne had proved the result in the commutative case, and Grothendieck had proved it when the base was reduced; Rene Schoof had proved it in more cases, and there had even been a paper by Emiliano Torti published last year, proving it in even more generality. I said that I thought that this was a fabulous thing to get AI thinking about.

But back to Akhil. I am not sure if he took my idea to disprove the Hodge conjecture seriously. But it looks like he had deeply understood that, with these extraordinary new AI tools, counterexamples might be low-hanging fruit right now. He had discussed with Levent Alpöge the idea of finding more counterexamples in algebraic geometry, and 12 hours ago Levent posted on X that Fable had found a counterexample to the Jacobian Conjecture . This is a big deal — this is a famous question in algebraic geometry which had been open for 100 years and which many people had thought about. It was apparently solved during the 2026 World Cup Final.

I actually find it easier to go through the formal output than the informal output. With the formal output, there is no danger of imagining things or misinterpreting the argument. Most reasonable Lean developments are organized into logical progressions of lemmas, and most of the lemmas might even be obvious to someone well versed in the field (who can also read Lean, of course), leaving only a small amount of actual argumentation to read.

The role of mathematicians is not just to prove conjectures, but also to formulate them. Formulating an interesting/important/useful statement that is a candidate for a theorem often requires as much creative insight (if not more) as does proving it.

Re human beings being “blind” — hindsight is a wonderful thing 🙂 Although I think it’s more accurate to say that the disproof is a highly nontrivial consequence of the basic fact that multiplication of a linear homogeneous polynomial and a quadratic homogeneous polynomial is not injective. There’s much more going on than that.