‘Ahead of his time’: AI helps unlock discoveries hidden in notebooks of man who transformed maths

The Austrian logician Kurt Gödel was one of the most original thinkers of the 20th century, whose incompleteness theorems published in 1931 transformed mathematics and paved the way for the digital age. Since 2017, Finnish logician Jan von Plato has led a project at Helsinki University to understand 16 notebooks Gödel wrote in the early 1940s, containing 1,009 pages of densely written text in the obsolete German shorthand Gabelsberger.

Progress was painfully slow – about a page a week – until September, when von Plato enlisted the help of the AI model Claude. Within days, Claude had provided a comprehensive digest of the entire material, revealing that Gödel had proved hundreds of theorems that no one knew about. 'I was flabbergasted,' said von Plato. 'The workbooks not only contain dozens of anticipations of results not known until the 70s and 80s, but they also contain 14 themes in logic that have not been pursued. Gödel was far ahead of his time.'

AI Revolutionizes Analysis

Von Plato received a €2.5m grant from the European Research Council for his Gödel project and taught himself Gabelsberger shorthand, noting 'I am one of only six people who can read it in the world.' At a conference in France about AI and theorem proving, he met computer scientists who suggested using Claude to analyze the workbooks.

On returning to Helsinki, von Plato began showing Claude his transcriptions of the workbooks, along with six books he had written on Gödel and other scientific literature. 'In a couple of days, I got to see a 650-page explanation of the workbooks. It had to be controlled page for page, but it's basically a work that is impossible for human beings to do,' he said. 'Humans read one page at a time and we tend to forget things. It takes us a year to read about 50 pages. We just are not able to keep in mind all the different parts.'

Rediscovering Lost Proofs

Gödel's incompleteness theorems revealed that in all mathematical systems there are true statements that can neither be proved nor disproved. In 1966, American mathematician Paul Cohen won the Fields medal for showing the independence of the axiom of choice. Gödel claimed he had already proved this result in the 1940s but couldn't reconstruct it when pressed by peers.

Von Plato tasked Claude with finding if Gödel's workbooks contained a proof of the independence of the axiom of choice. The AI found that Gödel was 'just one step away' from completing the proof. 'There's one definition that Gödel got wrong, but he had the right definition two years earlier,' von Plato explained. When the reconstructed proof was run through the proof assistant Coq, it passed verification.

Von Plato believes had Gödel published this work, he would have won the 1940 Fields medal. 'Maybe he felt that when Cohen got the medal, that that was something he sort of missed,' he suggested.

Hundreds of New Theorems

When von Plato asked Claude to extract all theorems in the workbooks for which Gödel had proofs, sketches, or ideas, the AI found 663. About 400 were verified as stated, 200 required minor repairs, and about 50 were false. 'Gödel himself, when rereading his notes, would occasionally add a marginal remark: falsch! or schlecht! [bad],' von Plato noted.

Joel David Hamkins, a professor of logic at the University of Notre Dame, commented that if the reconstructed proof stands up, 'it is remarkable and historically interesting.' He added, 'The fact that there are things in there that resemble [Cohen's proof] does not mean he had it. It shows he was on the path. You don't get credit for work you don't tell anyone about. But Gödel had so many ground-breaking ideas that it is maybe not surprising that his notebooks are full of exciting things.'

Von Plato plans to continue exploring Gödel's notebooks, including his physics and cosmology notebooks which he describes as 'an unknown territory.' 'I am sure the continued study of Gödel's manuscripts will reveal further treasures,' he concluded.