AI helps unlock discoveries hidden in Kurt Gödel's notebooks
Finnish logician Jan von Plato used the AI model Claude to analyse 16 notebooks of Austrian logician Kurt Gödel and found hundreds of previously unknown theorems. An independent professor says historians must judge how much of the result belongs to the AI and how much to Gödel.
Finnish logician Jan von Plato, a researcher at the University of Helsinki, used the AI model Claude in September to make sense of notebooks written in the early 1940s by the Austrian logician Kurt Gödel. The result was the discovery that Gödel had proved hundreds of theorems nobody knew about. Gödel's incompleteness theorems, published in 1931, transformed mathematics and paved the way for the digital age, which is why his unpublished papers interest historians of science.
Difficult material
Since 2017, von Plato has led a project to understand 16 notebooks known as the "workbooks". They contain 1,009 pages of dense text on maths and logic, much of it in Gabelsberger, a German shorthand that was already obsolete in Gödel's day. The project has a €2.5m grant from the European Research Council. Von Plato taught himself the shorthand and says only six people in the world can read it. Progress was initially very slow, at about a page a week.
What Claude found
After meeting computer scientists at a conference in France, von Plato showed the model his transcriptions, six of his own books on Gödel and other scientific literature. Within a couple of days he received a 650-page explanation, which had to be checked page by page.
Claude concluded that the notebooks contain an almost complete proof of the independence of the axiom of choice. In 1966, when Paul Cohen won the Fields medal for this result, Gödel claimed he had proved it in the 1940s but could not reconstruct a proof. According to von Plato, only one correct definition was missing. He ran the reconstructed proof through the proof assistant Coq, and it passed.
Overall, Claude extracted 663 theorems. About 400 were verified as stated, around 200 needed repair, and about 50 were false. Von Plato also says the notebooks contain 14 themes in logic that have not been pursued.
A cautious assessment
Joel David Hamkins, a professor of logic at the University of Notre Dame, has not seen the reconstruction but said that if it stands up, it is remarkable and historically interesting. He said it is a job for historians to determine how much is Claude and how much is Gödel, and that resemblance to Cohen's proof does not mean Gödel had it.
