Anthropic's Claude has done in days what would have taken a human scholar years: read through 1,009 pages of Kurt Gödel's unpublished notebooks and surfaced 663 theorems, proof sketches and ideas no one had ever catalogued. The findings, reported by The Guardian on November 13, suggest one of the 20th century's greatest mathematicians left behind a far larger legacy than scholars realised.
Gödel, famous for his incompleteness theorems of 1931, wrote 16 densely packed notebooks in the early 1940s after settling in Princeton. Much of the text is in Gabelsberger, a German shorthand already obsolete in Gödel's own lifetime. Since 2017, Finnish logician Jan von Plato has led a project at the University of Helsinki to study the notebooks, known as the "workbooks", teaching himself the shorthand and transcribing them at roughly one page a week.
The turning point came this summer. At a conference in France on AI and theorem proving, computer scientists suggested von Plato try Claude on the material. In September he gave the model his transcriptions, six books he had written about Gödel, and other scholarly literature. Within a couple of days, Claude returned a 650-page explanation — work von Plato said was beyond what any person could do alone.
663 theorems, checked one by one
Von Plato then asked Claude to extract every theorem for which Gödel had a proof, a sketch of one, or even an idea for one. The model produced a catalogue of 663 results. Each was then put through Coq, a program that formally checks mathematical proofs. About 400 passed exactly as stated. Around 200 needed repair — sharper wording or added assumptions — and about 50 turned out to be false, a pattern Gödel himself anticipated: some pages carry his own marginal verdicts, "falsch" (incorrect) and "schlecht" (bad).
The notebooks also contain results that anticipate mathematics only discovered decades later. Some predict findings that became known in the 1970s and 1980s, and the team identified 14 topics in logic that have still not been developed.
A proof Gödel never published
The headline find concerns the independence of the axiom of choice, a foundational question in set theory. Gödel claimed in 1966 that he had proved the axiom was independent of the system in which it was written, but he never published the proof. Paul Cohen later won the 1966 Fields Medal for the same result. Claude reconstructed a version of Gödel's argument from the notebooks — and found it contained a single definitional error. Once corrected, the proof passed Coq's checks. Von Plato noted that Gödel had used the correct definition two years earlier, suggesting he had come close to priority.
Not everyone is ready to rewrite the history books. Joel David Hamkins, a professor of logic at the University of Notre Dame, cautioned that he has not seen Claude's reconstruction, and that disentangling how much of the work is Gödel's and how much is the model's is "a job for the historians". The mathematical validity of the reconstructed proofs and their historical authorship, he said, are separate questions.
What this means for AI in research
Even with those caveats, the project is a striking demonstration of what AI can do for scholarship. A task that had consumed nine years of slow, page-by-page transcription was compressed into days of machine analysis — and formal checking with Coq gives the results a rigour a purely human reading could not match.
Hundreds of theorems are still being checked. But the harvest is clear: Gödel's notebooks hold far more mathematics than anyone knew, and an AI model helped bring it into the light.
