AI Reads a Dead Logician's Shorthand Notebooks in Two Days — Finds 663 Theorems Nobody Knew About

Claude processed 1,009 pages of Gödel's 1940s workbooks in Gabelsberger shorthand, surfacing hundreds of unpublished theorems and near-proof of the independence of the axiom of choice — 20 years before Cohen's Fields Medal.

Imagine you inherit a warehouse of filing cabinets from a genius inventor, but every document is written in a code only six people on Earth can read, and the pages cross-reference each other in ways no single human can hold in working memory. You could spend a career opening drawers one at a time, or you could build a machine that reads all the drawers at once and maps the connections. That's what just happened to Kurt Gödel's unpublished notebooks. Jan von Plato, a Finnish logician at Helsinki University, has spent since 2017 — backed by a €2.5 million European Research Council grant — leading a team to decode 16 workbooks Gödel filled in the early 1940s. The 1,009 pages are written in Gabelsberger, a German shorthand system already obsolete when Gödel used it. Von Plato is one of six people alive who can read it. Progress was roughly a page per week until September 2024, when von Plato fed his transcriptions and six of his own books on Gödel into Claude. Within two days, the model returned a 650-page digest of the entire corpus. The headline finding: Gödel proved far more than anyone knew. Claude identified 663 theorems for which Gödel had a proof, a sketch, or an idea. When these were run through the proof assistant Coq, approximately 400 verified as stated, about 200 required minor repairs (tighter definitions, added assumptions), and roughly 50 were false — consistent with Gödel's own marginal notes of "falsch!" and "schlecht!" The workbooks contain dozens of results that anticipate discoveries not published until the 1970s and 80s, plus 14 themes in logic and foundations of mathematics that remain unexplored 80-plus years later. The most dramatic claim concerns the independence of the axiom of choice. Paul Cohen won the 1966 Fields Medal for proving this independence. Gödel reportedly told colleagues he had already proved it in the 1940s but couldn't reconstruct the proof from his notes when pressed. Claude's reconstruction says he was one definition away — he had the correct definition two years earlier in the same notebooks but used an incorrect one at the critical step. Von Plato ran the reconstructed proof through Coq and reports it passed. He believes Gödel would have won the 1940 Fields Medal had he published. The methodological core here is not the AI "doing mathematics." Claude didn't prove new theorems. It performed large-scale cross-referencing and synthesis across a thousand pages of technical material — the kind of integrative reading that exceeds human working memory. Von Plato is explicit: "Humans read one page at a time and we tend to forget things. The AI can connect all the pieces in a thousand pages." This is corpus comprehension at scale, not theorem generation. The verification layer — Coq — is doing the actual mathematical gatekeeping. Joel David Hamkins of Notre Dame offers the appropriate caution: resembling a proof path is not the same as having it. "You don't get credit for work you don't tell anyone about," he notes. The question of how much is Claude's reconstruction versus Gödel's actual reasoning is genuinely open and will require careful historical adjudication. But Hamkins also concedes that given Gödel's track record, "it is maybe not surprising that his notebooks are full of exciting things." Von Plato plans to extend the approach to Gödel's physics and cosmology notebooks, which remain unexplored territory. The broader implication is clear: AI-assisted corpus analysis could unlock similar discoveries across the unpublished archives of other major thinkers — wherever dense, cross-referencing technical manuscripts exceed a single scholar's integrative capacity.