While OpenAI released hundreds of AI-generated mathematical proofs without warning earlier this week, Tom Verhoeff has instead spent the past year working intensively with AI models to find a solution to a problem that has occupied him for decades. Yet he, too, is seeing how rapidly the technology is evolving and how much AI is increasingly capable of doing on its own.
Imagine six dancers standing in a row. At each step, two neighboring dancers swap places. Can you visit every possible arrangement exactly once without repeating an earlier one? Yes, mathematicians have known that this is possible since the 17th century. But what if some of the dancers look identical, for example, two dressed in green, two in blue and two in yellow? In 1965, American mathematician D.H. Lehmer conjectured that this should still be possible, apart from a few small, predetermined detours. A proof remained elusive for the next 60 years.
Tom Verhoeff , a retired mathematician and computer scientist at Eindhoven University of Technology (TU/e), solved the binary case back in 2017, involving two different types of symbols ("colours"). He has now used AI to solve the general case as well: even when several types of symbols occur in different numbers, the desired sequence can still be constructed. This proves Lehmer's permutation conjecture, as Verhoeff himself has dubbed it. The biggest breakthrough came only a few weeks ago.
100,000 lines reduced to 35,000
A mathematical proof is not only about whether something is true, but also about how you demonstrate it. A proof of hundreds of pages may be correct, but a much shorter proof can reveal the underlying structure of a problem much more clearly.
Verhoeff's first proof ran to around 150 pages. It was also formally verified in Lean, a computer system that automatically checks every step of a mathematical proof. That verification comprised more than 100,000 lines of code.
Last September, Verhoeff asked Anthropic's new Claude Opus 5.5 model to start from scratch. Within a few hours, it came up with two new key ideas: dividing all possible arrangements into well-structured blocks and then cleverly connecting those blocks.
The proof is now less than 30 pages long, while the Lean verification has been reduced to around 35,000 lines of code.
'Proof that AI is developing at breakneck speed'
The new proof is not a shortened version of the old one. Verhoeff did not give the model the long proof as a starting point, but simply challenged it to solve the problem from scratch. "The long proof emerged in close collaboration with me, the shorter proof was produced autonomously," says Verhoeff. "I actually tried that in March as well, but it did not yield anything useful at the time."
"That shows that the mathematical abilities of AI models are developing at a tremendous pace", Verhoeff says. "This is a game changer much bigger than the arrival of electronic calculators or computer algebra systems. It forces us to rethink teaching and doing research at TU/e and elsewhere. We can't afford to sit back and wait."
Who did what?
The key ideas behind the simpler proof came from Claude Opus 5.5. The AI model DeepSeek V4.1 Flash then translated the various steps of the proof into a program that executes the reasoning and checks it against concrete examples.
Those computations were carried out on Spike-1, TU/e's supercomputer . "That computing power made it possible to run the cycle from AI output to human checking, back to a new question for the model and checking again, fast enough to complete the proof," says Verhoeff. The Aristotle system, developed by Harmonic, subsequently generated formal verification in Lean.
According to Verhoeff, advanced AI models were still unable to do serious mathematics in December last year. "GPT-5.2 (by OpenAI -ed.) still made very elementary mistakes. By May, things were already different. Anthropic's Opus 4.7 demonstrated mature mathematical understanding and could serve as a diligent assistant at an advanced level. But what truly surprised me was Opus 5.5, which could solve the problem autonomously."
A mountain of proofs
The models referred to here are publicly available. The models AI companies use internally are already more advanced. This is illustrated by the recent news that OpenAI used an internal model to solve, or at least make progress towards solving, hundreds of mathematical problems . Lehmer's permutation conjecture is not among them, by the way.
Verhoeff says: "If you look at the list of problems that OpenAI says it has solved, there is almost nothing on it that is familiar to me as a mathematician, let alone something that would be understandable to a wider audience. A problem in combinatorics that I have worked on may be difficult for a layperson to grasp, but the OpenAI list strikes me as truly esoteric. The question is how such an enormous mountain of problems helps mathematics move forward. And from what I hear, it is not particularly accessible in the way it is written either."
Verhoeff has submitted the solution as a preprint to arXiv , allowing others to study and scrutinize the proof.
