Claude decodes Gödel's shorthand notebooks and surfaces hundreds of unknown theorems

What happened

A long-running effort to decipher Kurt Gödel's unpublished notebooks took a sudden leap forward after the researcher leading it began working with the AI model Claude. According to The Guardian, within a couple of days the model produced a comprehensive analysis of 1,009 pages of notes the logician wrote in the early 1940s, showing that Gödel had proved far more than anyone realised.

The material is a set of 16 volumes known as the "workbooks", much of it written in Gabelsberger, a German shorthand that was already obsolete when Gödel used it. Since 2017 the Finnish logician Jan von Plato has led a project at the University of Helsinki to make sense of them, backed by a €2.5m European Research Council grant. Progress was glacial: human reading managed roughly a page a week, or about 50 pages a year.

The turning point came in August at a conference in France on AI and theorem proving, where computer scientists suggested von Plato try Claude. He gave the model his transcriptions of the workbooks, together with six books he had written on Gödel and other secondary literature. The result, The Guardian reports, was a 650-page explanation of the notebooks produced in days — one that still had to be checked page by page, but which von Plato described as a task beyond human capability, since no reader can hold a thousand pages of dense logic in mind at once.

The axiom of choice question

The most striking finding concerns the axiom of choice. In 1966 Paul Cohen won the Fields Medal for showing that the axiom of choice and the continuum hypothesis are independent of standard set theory. Gödel responded by claiming he had proved the independence result himself in the 1940s, but he could not reconstruct the proof when colleagues pressed him.

Von Plato's first question to Claude was whether the workbooks contained such a proof. The answer, in his words, was "yes, almost": Gödel had one definition wrong, though he had stated the correct version two years earlier, and von Plato believes a few more months of work would have got him there. The reconstructed argument was then run through Coq, a proof assistant that mechanically verifies mathematical proofs, and it passed. Von Plato suggests Gödel would have won the 1940 Fields Medal had he published the work.

663 theorems, machine-checked

Von Plato also asked Claude to pull out every theorem in the workbooks for which Gödel had a proof, a proof sketch or the germ of an idea. The model found 663. Checked in Coq, about 400 were verified as stated, roughly 200 were repaired — their statements sharpened or extra assumptions added — and about 50 were false. As The Guardian points out, Gödel himself sometimes flagged his own errors in the margins with remarks such as "falsch!" or "schlecht!".

Beyond individual results, von Plato says the workbooks contain dozens of anticipations of findings not discovered until the 1970s and 80s, along with 14 themes in logic that have never been pursued. Gödel's physics and cosmology notebooks, still largely unexplored, are next on his list.

A note of caution

Not everyone is prepared to rewrite the history books yet. Joel David Hamkins, a professor of logic at the University of Notre Dame, told The Guardian he has not seen Claude's reconstruction of the axiom-of-choice proof. If it holds up it would be "remarkable and historically interesting", he said, but disentangling what is Claude's contribution from what is Gödel's is a job for historians. Notebook passages resembling Cohen's proof show Gödel was on the path, Hamkins argued — but unpublished work earns no credit.

Why it matters

The story is a concrete demonstration of where AI is genuinely useful in scholarship: processing volume and making connections across material that exceeds human capacity. A corpus whose human progress was measured in pages per week was digested in days, in a shorthand only a handful of people alive can read. Just as important is the verification pattern — the language model proposed reconstructions and extractions, while an independent proof assistant checked them, mitigating the reliability problems that make raw model output risky in mathematics. If the method generalises, other undeciphered or under-studied scientific archives may soon become newly readable, and some long-settled priority questions in the history of mathematics may need revisiting.