Claude has identified 663 proof-related entries in Austrian logician Kurt Gödel’s notebooks, giving researchers a way to examine a mathematical archive that has been difficult to work through by hand.
Jan von Plato, who led the project, described the findings in an account published by The Guardian. He said the AI model Claude located entries that ranged from completed proofs to proof sketches and ideas for proofs.
Von Plato said about 400 entries were verified in Coq as stated. Roughly 200 were repaired, while about 50 were false. The 663 entries therefore do not represent 663 completed proofs.
Much of the 1,009-page collection uses Gabelsberger, a German shorthand that was already obsolete when Gödel wrote in it. His unpublished manuscripts total tens of thousands of pages. The archive has drawn interest from historians of science, while its notation has posed a practical hurdle to reading it.
The project addresses the slow pace of examining the material. Von Plato said human review was advancing at roughly a page per week and that it took people about a year to read 50 pages. Claude could connect material across the workbooks, according to his account.
Gödel produced only a small number of papers after his major work in the 1930s. His two incompleteness theorems, published in 1931, reshaped mathematics and helped lay intellectual groundwork for the digital age.
The report also revisits a 1966 claim by Gödel that he had proved the independence of the axiom of choice in the 1940s. Von Plato said Gödel’s notes used one incorrect definition, but Claude’s reconstructed proof passed Coq verification. Mathematician Joel David Hamkins said he had not seen the reconstruction and questioned how much of it should be credited to Gödel and how much to Claude.
After finishing his current logic projects, von Plato plans to examine Gödel’s notebooks on physics and cosmology. The report gave no date for that next stage.
