AI Claude finds hundreds of previously unknown theorems in Gödel's notebooks
Finnish logician Jan von Plato used the AI model Claude to analyse 1,009 pages of notebooks by Austrian logician Kurt Gödel within days. They appear to contain hundreds of theorems nobody knew about, and many have been checked with a proof assistant.
Jan von Plato, a Finnish logician at the University of Helsinki, has used the AI model Claude, developed by Anthropic, to digest 16 notebooks by the Austrian logician Kurt Gödel, known as the "workbooks". Gödel wrote them in the early 1940s. The analysis indicates he had proved hundreds of theorems that were previously unknown. The finding matters for the history of mathematics, since Gödel's 1931 incompleteness theorems transformed the subject and paved the way for the digital age.
A difficult source
After his early landmark results, Gödel published only a few papers, yet his unpublished writings run to tens of thousands of pages. Since 2017, von Plato has led a project to understand the workbooks, which total 1,009 densely written pages on maths and logic. Much is in Gabelsberger, a German shorthand that was already obsolete in Gödel's day. The project is funded by a €2.5m grant from the European Research Council, and von Plato taught himself the shorthand and assembled a small team. Progress was slow, at roughly one page a week.
In September, after a conference in France on AI and theorem proving, he showed Claude his transcriptions and six of his earlier books on Gödel. Within a couple of days he had a 650-page explanation of the workbooks.
Results
Von Plato asked the model to extract every theorem for which Gödel had a proof, a sketch or an idea for a proof. Claude found 663. When checked in Coq, a program that verifies mathematical proofs, about 400 held as stated, about 200 needed repairs and roughly 50 were false. Von Plato says the notebooks also contain 14 themes in logic that have not been pursued, and several results that other researchers only reached in the 1970s and 80s.
One early task was to see whether the notebooks contained a proof of the independence of the axiom of choice. In 1966 the American mathematician Paul Cohen won the Fields medal for such a result, and Gödel then claimed he had proved it in the 1940s. Claude's answer was "almost": Gödel was one step away because of one incorrect definition.
Joel David Hamkins, a logic professor at the University of Notre Dame in Indiana, said that if the reconstruction stands up it would be interesting, but that historians must determine how much of it is Claude and how much is Gödel.
