How a mathematician watched AI grow from servant to grandmaster

Imagine six dancers standing in a row. Each time, two neighbours swap places. Can you cycle through every possible arrangement exactly once, without repeating any earlier arrangements? Yes, you can, as mathematicians have known since the 17th century. But what if some of the dancers look identical — for example, two in green, two in blue and two in yellow? In 1965, American mathematician D.H. Lehmer conjectured that such a cycle would still be possible, apart from a few small, predetermined detours. Yet a proof remained elusive for sixty years.

Tom Verhoeff, a retired mathematician and computer scientist at Eindhoven University of Technology (TU/e), solved the binary case in 2017, involving two different types of symbols (‘colours’). Now, with the help of AI, he has also solved the general case: even when several types of symbols occur in all sorts of different quantities, the required cycle can be constructed. This proves what Verhoeff himself has named Lehmer’s permutation conjecture. The biggest breakthrough came just a few weeks ago.

While OpenAI released hundreds of AI-discovered mathematical proofs into the world without warning this week, Tom Verhoeff spent the past year working closely with AI models to find a solution to one specific problem that had occupied him for decades. Yet he, too, sees how quickly the technology is advancing and how much AI is increasingly accomplishing independently.

From 100,000 lines to 35,000

A mathematical proof is not just about whether something is true, but also about how you demonstrate it. A proof running to hundreds of pages may be correct, but a much shorter proof can reveal a better understanding of the underlying structure.

Verhoeff’s first solution ran to around 150 pages. The proof was also formally checked in Lean, a computer system that automatically verifies every step of a mathematical proof. That verification involved more than 100,000 lines.

This September, Verhoeff asked Claude Opus 5.5, the new model from AI company Anthropic, to start completely afresh. Within a few hours, it came up with two new core ideas: divide all the arrangements into neatly structured blocks, then connect those blocks cleverly. The proof is now fewer than 30 pages long, and the Lean verification has been reduced to around 35,000 lines.

‘Proof that AI is advancing at a remarkable pace’

The new proof is not an abridged 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 was developed in close collaboration with me; the shorter proof was produced autonomously,” he says. “Incidentally, I had also tried that in March, but it yielded nothing useful at the time.”

“This shows that the mathematical abilities of AI models are advancing at a remarkable pace,” Verhoeff says. “This is changing the field far more profoundly than the arrival of the calculator in the 1970s or computer algebra systems in the 1980s. It forces us to rethink how we teach mathematics and conduct research at TU/e and elsewhere. We cannot afford to simply let things take their course.”

Six dancers in three colours, two of each colour, repeatedly swap places with a neighbour. Each row represents one arrangement. After 96 steps, every arrangement has appeared and you are back at the start. The double lines mark the six unavoidable detours. The shaded areas show the blocks into which the AI model Opus 5.5 divided the arrangements — an idea the model came up with independently. Illustration: © Tom Verhoeff

Who did what?

Claude Opus 5.5 generated the core ideas behind the simple proof. The AI model DeepSeek V4.1 Flash then translated the proof's steps into a program that carries out the reasoning and checks it against concrete examples.

The team performed those computations on Spike-1, TU/e’s supercomputer. “That computing power allowed us to move through the cycle of AI output, human checking, a new question to the model and further checking quickly enough to complete the proof,” Verhoeff says. Harmonic’s Aristotle system then wrote the formal verification in Lean.

According to Verhoeff, advanced AI models still couldn't do serious mathematics in December last year. “GPT-5.2 (from OpenAI — ed.) was still making very basic mistakes. By May, things had changed: Anthropic’s Opus 4.7 demonstrated a mature understanding and could act as an advanced assistant. But Opus 5.5 really surprised me: it managed to solve the problem autonomously.”

A mountain of solutions

These are publicly available models. The models AI companies have internally are already further ahead. One indication is the news that OpenAI used an internal model to solve hundreds of mathematical problems, or at least move closer to a solution. Lehmer’s permutation conjecture, incidentally, is not among them.

Verhoeff: “If you look at the list of problems OpenAI says it has solved, there is virtually nothing that seems familiar to me as a mathematician, let alone anything a wider audience could understand. 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 results advances mathematics. And from what I hear, they have not been written up in a very accessible way either.”

Verhoeff has submitted the solution to ‘his’ problem as a preprint on arXiv, allowing others to study the proof.

(Based on a press release from Eindhoven University of Technology)