Artificial intelligence has helped researchers unlock hundreds of previously unknown mathematical theorems hidden inside the notebooks of Austrian logician Kurt Gödel, as reported by The Guardian. Gödel left behind 1,009 pages of densely written text in an obsolete German shorthand, which Finnish logician Jan von Plato and his team at Helsinki University have been studying since 2017.
Unlocking Obsolete Shorthand With AI
Progress on translating the 16 notebooks, known as workbooks, crawled at about a page a week due to the complex Gabelsberger shorthand. In September, von Plato enlisted the AI model Claude to assist with the material. Within a couple of days, Claude generated a comprehensive 650-page explanation of the entire text.
Jan von Plato told The Guardian that he was flabbergasted by the results, noting that the workbooks contain anticipations of results not known until the 1970s and 1980s, alongside 14 unexplored themes in logic. He stated that the AI can connect pieces across a thousand pages and view Gödel’s writings as a single piece, a task impossible for humans who read one page at a time and forget details.
Proving Unfinished Theorems
The first task assigned to Claude was investigating whether Gödel’s notes contained a proof of the independence of the axiom of choice, a milestone that earned American mathematician Paul Cohen a Fields medal in 1966. Gödel had claimed at the time that he already proved it in the 1940s, but could not reconstruct a proof. Claude found that Gödel was just one step away, having made a minor error in a definition.
Von Plato ran Claude’s reconstructed proof through Coq, a program that verifies mathematical proofs, and it passed successfully. When von Plato asked Claude to extract all theorems where Gödel had a proof, sketch, or idea, the AI found 663 theorems. Coq verified about 400 as stated, repaired around 200, and found about 50 to be false, which matched Gödel’s own marginal notes labeling some ideas bad or false.
Joel David Hamkins, a professor of logic at the University of Notre Dame, noted that while items resembling Cohen’s proof show Gödel was on the correct path, historians must determine how much credit belongs to Claude versus Gödel.
Jan von Plato plans to continue studying Gödel’s manuscripts for unexplored themes in logic and foundations of mathematics, and eventually hopes to explore the logician’s unknown physics and cosmology notebooks.
