Tuesday, April 28, 2026

21st Century Mathematics: The Unfolding of the Proof of Erdös Problem 1196 by a Generative AI Model

It's April 13th 2026. Liam Price words a short, simple prompt into ChatGPT-5.4 and hits the jackpot: For the first time one such GenAI models, in a single shot, developed a proof of a Mathematical conjecture that so far had escaped Mathematicians, and it did so using a novel approach that had been sidelined in the literature before.

The proof was then verified in Lean, a discussion unearthing insights from the AI-dumped proof followed, and a famous mathematician, Terence Tao, came up with a different, simpler proof of Erdös conjecture, all in the span of two days.

You can read how the whole story unfolded from the actual discussion the mathematicians had:

https://www.erdosproblems.com/forum/thread/1196?order=oldest

And Price did hit the jackpot: in the discussion that ensued after he announced the finding, it was suggested to "reproduce" said proof by asking the same and other chatbots for a proof. They failed to find any proof at all in 8 out of 10 trials, while the remaining proofs required several additional prompts  where mathematicians hinted the model [1].

But this event carries the signs of an historical moment. It showcased what will likely become a trait mark of tomorrow's Mathematics: 

1. Some "AI" model spits out a potential proof of a theorem. Such an event, in itself, is very close to useless for the human race, let alone the rest of Nature!

2. Humans, in the form and shape of mathematicians -for now-, verify the proof in a proof assistant, like Lean. The proof, now, acquired some tangible value.

3. At the same time, they and others try to find some insights into how the proof works, how to build an intuition around it and, the cherry on the top, eventually find a simpler, more intuitive proof. At this point, the event at step 1) gathers all the possible value it can get: it becomes yet another stepping stone upon which humans widened their knowledge.

I didn't say it first, but a recognized, worldwide authority as Tao:  https://mathstodon.xyz/@tao/116477351524980995

Welcome to the Mathematics of the 21st century!

PS: A word of caution: GenAIs are still stupid. If you throw them around without thinking, you will hurt someone the same way as you would if you blindly throw a hammer at a group of people.


[1] What counts as the first proof ever of a mathematical conjecture by an AI happened in February 2026, although it wasn't in a single shot, but required human assistance, and the method laid out by the model had close similarities to those employed in obtaining similar results in the literature. See Tao's summary  https://mathstodon.xyz/@tao/115855840223258103

No comments:

Post a Comment