Claude Read 1,009 Pages of Gödel's Obsolete Shorthand in Days: 663 Theorems, About 400 Verified in Coq

Kurt Gödel left behind tens of thousands of pages he never published, including 16 workbooks from the early 1940s — 1,009 pages of mathematics and logic written largely in Gabelsberger, a German shorthand that was already obsolete while he was using it. For seven years, Finnish logician Jan von Plato of the University of Helsinki transcribed them at a pace of about a page a week. In September, he gave the transcripts to Claude. Within days, the model returned a 650-page analysis of the entire corpus.

The results, reported by The Guardian, suggest the most famous logician of the twentieth century was even further ahead of his time than historians believed. The analysis identified 663 theorems for which Gödel had written a proof, a proof sketch or a concrete idea — results no one knew about. Von Plato said the workbooks contain dozens of anticipations of theorems not published until the 1970s and 1980s, plus 14 themes in logic that have still never been pursued.

The claims were not taken on the model's word. Von Plato ran the extracted results through Coq, a proof assistant that mechanically checks mathematical arguments. About 400 of the 663 theorems were verified exactly as stated; roughly 200 required repaired definitions or added assumptions to go through; and about 50 turned out to be false. That triage — machine extraction, machine verification, human review page by page — is what separates this from an AI hallucination story.

The centerpiece is historical. In 1966, Paul Cohen won the Fields Medal for proving that the axiom of choice is independent of standard set theory, and Gödel reacted by saying he had proved the same result in the 1940s but could no longer reconstruct the argument from his notes. Von Plato asked Claude whether the workbooks held the missing proof. The answer was "yes, almost": one definition was wrong, but Gödel had written down the correct one two years earlier. The reconstructed proof passed Coq.

Von Plato, who is one of only six people in the world who can read Gabelsberger, argues the significance is about scale rather than intelligence: humans read a thousand pages one at a time and forget; the model can hold the whole corpus as one connected work. "It's basically a work that is impossible to do for human beings," he told The Guardian. The project is funded by a 2.5 million euro grant from the European Research Council.

Outside logicians are more measured. Joel David Hamkins of the University of Notre Dame, who has not seen the reconstruction, said the result would be outstanding and historically interesting if confirmed — but stressed that historians still have to establish how much of the finished proof is Gödel's own thought and how much is the model's interpolation. Von Plato's suggestion that Gödel would have won a 1940 Fields Medal had he published is opinion, not verified fact.

The Gödel workbooks are the clearest demonstration yet of a pattern running through this year's AI-for-science results: long-context models are not better mathematicians than specialists, but they can connect fragments across a corpus no human can hold in mind at once — and, paired with a formal verifier like Coq, their output can be made checkable rather than merely plausible. What remains, deciding what belongs to Gödel and what belongs to the machine, is now a problem for historians of mathematics.