Claude and Gödel’s workbooks (von Plato)

Your AI and this story

Key facts

• Material: 16 workbooks written after Gödel settled in Princeton in 1940, 1,009 pages, much of it in Gabelsberger shorthand; the project (since 2017, €2.5m European Research Council grant) had progressed at ‘about a page a week’
• AI step: in August 2026, at a conference on AI and theorem proving in France, computer scientists suggested Claude; von Plato gave it his transcriptions, six of his books on Gödel and secondary literature. ‘In a couple of days, I got to see a 650-page explanation of the workbooks. It had to be controlled page for page, but it’s basically a work that is impossible to do for human beings’ (von Plato, The Guardian)
• Axiom of choice: Gödel told colleagues after Paul Cohen’s 1966 Fields Medal that he had proved the independence result in the 1940s but could not reconstruct the proof. Von Plato: ‘He was just one step away … There’s one definition that Gödel got wrong, but he had the right definition two years earlier’; the reconstructed proof, he says, passed Coq
• Census: Claude listed 663 theorems for which Gödel had a proof, a sketch or an idea; in Coq ‘About 400 were verified as stated, about 200 were repaired … About 50 were false’ (von Plato); Claude also lists ‘more than a dozen’ (14) logic themes not pursued since
• Sceptic: Joel David Hamkins (Notre Dame), who had not seen the reconstruction: if it stands up ‘it is remarkable and historically interesting. Although how much is Claude and how much is Gödel is a job for the historians’; ‘You don’t get credit for work you don’t tell anyone about’
• Not stated: which Claude model or interface was used, whether Anthropic was involved, where the Coq files are; no preprint, repository or Helsinki press release found by 14 Nov. Von Plato’s AITP 2026 slides (‘Deciphering Gödel’) describe the shorthand and three example results, including a Gödel claim shown false by a counterexample whose correction gives a new result relating classical and intuitionistic logic, and say ‘AI methods would likely lead to an understanding of Gödel’s own proof’
• Secondary reports add (unverified, no source given): a 1,084-page expanded digest, ‘55’ false results, a reading by set theorist Akihiro Kanamori and formal-verification help from Josef Urban (36Kr repost, 14 Nov)
• Reach: Hacker News front page (421 points, 13 Nov); commenters disputed how much new mathematics the notebooks can still hold and whether the work is mainly transcription