“I was flabbergasted,” said Jan von Plato.
Artificial intelligence has helped unlock hundreds of previously unknown mathematical theorems hidden within the dense, obsolete shorthand notebooks of Austrian logician Kurt Gödel, The Guardian reported on November 13.
Gödel transformed modern mathematics with his two incompleteness theorems published in 1931, which revealed the inherent limits of mathematical knowledge and eventually inspired Alan Turing’s 1936 paper laying the groundwork for modern computation. While his published works remained relatively few, his handwritten archive spanned tens of thousands of pages, presenting a formidable challenge to historians of science.
Since 2017, von Plato, a logician at Helsinki University, has led an effort to decipher 1,009 pages of mathematical notes contained within 16 notebooks written by Gödel in the early 1940s. Much of the text was recorded in Gabelsberger, a German shorthand system that was already obsolete during Gödel’s lifetime.
Progress on the manuscripts crept along at a rate of roughly one page per week. That pace changed drastically in September, when von Plato enlisted the help of the AI model Claude.
Within days, Claude delivered a comprehensive 650-page breakdown of the entire corpus. “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 to do for human beings,” Jan von Plato, a logician at Helsinki University, said.
The AI model identified 663 theorems for which Gödel possessed a proof, a sketch, or a conceptual outline. When those results were tested using Coq, a program designed to verify mathematical proofs, about 400 were validated as stated, roughly 200 required minor precision adjustments or added assumptions, and about 50 were incorrect.
The analysis also shed light on a historical dispute surrounding the axiom of choice. In 1966, American mathematician Paul Cohen earned a Fields Medal for proving the independence of the continuum hypothesis and the axiom of choice—a result Gödel maintained he had already achieved in the 1940s, though he failed to reconstruct the proof when pressed by his peers.
When von Plato tasked Claude with examining the notebooks for this proof, the model determined that Gödel was just one step away, having relied on a definition he had successfully altered two years prior. “it is remarkable and historically interesting. Although how much is Claude and how much is Gödel is a job for the historians,” Joel David Hamkins, a professor of logic at the University of Notre Dame, said, noting that while the findings place Gödel close to the path of discovery, historians must still determine the exact boundary between Gödel's notes and Claude's computational reconstruction.
Von Plato plans to continue examining the manuscripts, noting that the notebooks contain more than a dozen unexplored themes in logic alongside untouched physics and cosmology notes.
