Berliner Tageblatt - AI Unlocks Hundreds of Proved Theorems in Kurt Gödel’s Hidden Notebooks

A Finnish logician has utilized artificial intelligence to decode a vast collection of unpublished manuscripts by Kurt Gödel, revealing hundreds of proved theorems that had remained hidden for decades. The work demonstrates that the Austrian logician, already renowned for his incompleteness theorems, possessed insights into mathematical logic that predated discoveries made in the 1970s and 1980s.

Jan von Plato, a professor at Helsinki University, has led a project since 2017 to analyze 16 notebooks written by Gödel in the early 1940s. The collection comprises 1,009 pages of densely written text concerning mathematics and logic. A significant portion of this material is composed in Gabelsberger, an obsolete German shorthand system that was already considered outdated during Gödel’s lifetime.

Progress in deciphering these notebooks was historically slow. Von Plato, who taught himself the shorthand script—claiming to be one of only six people worldwide capable of reading it—along with a small team, could process approximately one page per week. The effort required immense patience, as human readers tend to lose context when navigating such complex, fragmented texts over extended periods.

The breakthrough occurred in September when von Plato integrated the AI model Claude into the research process. After providing the model with his transcriptions of the workbooks and six books he had previously authored on Gödel and related scientific literature, von Plato received a comprehensive 650-page digest of the material within two days.

"In a couple of days, I got to see a 650-page explanation of the workbooks," von Plato said. "It had to be controlled page for page, but it’s basically a work that is impossible to do for human beings. 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. The AI can connect all the pieces in a thousand pages. It can see all of Gödel’s writings as one piece."

The analysis revealed that Gödel had proved hundreds of theorems that were previously unknown to the mathematical community. When von Plato asked Claude to extract every theorem for which Gödel had provided a proof, sketched a proof, or outlined an idea, the AI identified 663 such results.

These findings were subsequently verified using Coq, a program designed to validate the correctness of mathematical proofs. The verification process yielded specific outcomes: approximately 400 theorems were confirmed as stated; about 200 required minor repairs, such as more precise statements or additional assumptions; and roughly 50 were found to be false. Von Plato noted that Gödel himself had occasionally marked his notes with "falsch" (incorrect) or "schlecht" (bad) when rereading them.

Among the most significant discoveries was a reconstruction of Gödel’s proof regarding the independence of the axiom of choice. In 1966, American mathematician Paul Cohen received the Fields Medal for demonstrating this independence. Gödel had previously claimed to have proven the result in the 1940s but could not produce a formal proof when pressed by peers.

Claude’s reconstruction showed that Gödel was "just one step away" from a complete proof, having made an error in one definition despite having the correct definition two years earlier. Von Plato ran the AI-generated proof through Coq, where it passed verification. He suggested that if Gödel had published this work, he might have been awarded the 1940 Fields Medal.

"What strikes me especially is that he starts from ideas," von Plato said. "He’s not like someone who plays with formulas and hopes to arrive somewhere. He has very, very clear ideas, and then he’s methodical. Step after step he goes ahead and he manages to fulfil the aims that he has in this formal work."

The AI analysis also identified 14 themes in logic that had not been pursued by other mathematicians in the 80-plus years since Gödel wrote them down. Von Plato described these as "treasures" that warrant further exploration, alongside Gödel’s notebooks on physics and cosmology, which he plans to examine after completing his current logic projects.

Von Plato initiated the project in 2017 while facing mandatory retirement from Helsinki University. He secured a €2.5 million grant from the European Research Council to support the effort, driven by a desire to remain academically active. "What should I do to make myself indispensable? Oh yes, I’ll start reading Gödel’s enigmatic shorthand pages!" he recalled.

The implications of these findings have drawn attention from the broader logic community. Joel David Hamkins, a professor of logic at the University of Notre Dame in Indiana, noted that while he had not seen the full reconstruction, the results would be historically significant if they held up to scrutiny.

"Although how much is Claude and how much is Gödel is a job for the historians," Hamkins said. "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."

Gödel, who fled Austria under Nazi rule in 1940 and settled in Princeton, New Jersey, became a close friend of Albert Einstein at the Institute for Advanced Study. His earlier work on the incompleteness theorems, published in 1931, demonstrated that within any mathematical system, there are true statements that cannot be proved or disproved within that system. This revelation shifted the trajectory of logic and computation, inspiring Alan Turing’s foundational work in 1936.

Von Plato remains "flabbergasted" by the depth of Gödel’s foresight. "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," he said. "Gödel was far ahead of his time."

While the AI has provided a powerful tool for decoding Gödel’s dense shorthand, the project underscores the enduring complexity of interpreting unpublished scientific manuscripts. The collaboration between human expertise in historical context and computational power in pattern recognition has opened new avenues for understanding one of the 20th century’s most original thinkers.

N.Fournier--BTB