Marc Lackenby is a topologist. He's been working on hard problems in group theory for years.
Last year, he fed Problem 21.10 from the Kourovka Notebook into a new AI system from Google DeepMind.
The Kourovka Notebook is a famous list of open problems. Mathematicians have been adding to it for years. Problem 21.10 was just sitting there, unsolved.
The AI worked on it. Came back with a proof. Then flagged its own proof as broken.
One of the system's internal reviewer agents had read the argument, found a flaw, rejected it. So the workstream got marked unfinished.
Most demos would call this a failure. Lackenby didn't.
He read the rejected proof anyway. And inside it, he found what he later called a "really, really clever" strategy. Then he read the reviewer's critique of why the proof had failed.
And he saw it. He knew exactly how to fix the gap.
So he told the system what to do. The system wrote up a complete proof. He downloaded it. Generalized the result a little. Added some examples. Uploaded it again. Asked the coordinator to run a final review.


