University of Helsinki · 2026-11-13 · major
Gödel's notebooks — Claude finds 663 theorems in 1,009 shorthand pages
In short
Helsinki logician Jan von Plato used Claude to read his transcriptions of Kurt Gödel's 1940s workbooks. Claude listed 663 theorems; in the Coq proof checker about 400 held as stated, 200 needed repair and 50 were false.
University of Helsinki · 2026-11-13 · 3 sources checked

Claude turned a slow, page-a-week reading of Gödel's private workbooks into a full catalogue of his unpublished theorems.
Quick facts
| Project lead | Jan von Plato, University of Helsinki |
|---|---|
| Source material | 16 Gödel workbooks, early 1940s, 1,009 pages |
| AI used | Claude, from September 2026 |
| Theorems found | 663 proved, sketched or outlined |
| Coq check | ~400 verified, ~200 repaired, ~50 false |
| Human pace before | About one page a week |
What is it?
Kurt Gödel's 16 workbooks from the early 1940s hold 1,009 pages on maths and logic, much of it in Gabelsberger, a German shorthand that was already obsolete. Jan von Plato's Helsinki project had read them at about one page a week since 2017. With Claude, it now has a list of 663 theorems Gödel proved, sketched or had an idea for.
How does it work?
Von Plato gave the model his transcriptions plus six of his own books on Gödel, and got back a 650-page digest that he checked by hand. He then had the extracted results tested in Coq, a program that checks mathematical proofs. The first target was Gödel's 1966 claim that he had proved the independence of the axiom of choice in the 1940s: the notebooks held a proof that was one definition short.
Why does it matter?
Long-context reading is the useful part here: von Plato says humans read one page at a time and forget, while the model could connect all thousand pages at once. Pairing a language model with a formal proof checker gave a way to sort real results from false ones. Claude also flagged more than a dozen logic themes in the workbooks that no one has followed up.
Who is it for?
mathematicians, historians of science and anyone using AI on archives
Frequently asked questions
- Did Claude read Gödel's shorthand handwriting itself?
- No. Jan von Plato, who taught himself Gabelsberger shorthand for the project, gave Claude his own transcriptions of Gödel's workbooks, six of his books on Gödel and other secondary literature. Claude then produced a 650-page explanation of the workbooks in a couple of days, which von Plato says had to be checked page by page.
- Did Gödel really prove the independence of the axiom of choice?
- Almost, according to von Plato. Claude found a nearly complete proof in Gödel's workbooks with one wrong definition, and Gödel had written the right definition two years earlier. Von Plato says the repaired proof passed the Coq proof assistant. Paul Cohen won the 1966 Fields medal for proving that result.
- What do other mathematicians say about the Claude Gödel findings?
- Joel David Hamkins, a logic professor at Notre Dame who had not seen the reconstruction, told the Guardian that if it stands up it is remarkable and historically interesting. He added that how much is Claude and how much is Gödel is a job for historians, and that resembling Cohen's proof does not mean Gödel had it.
- Were all 663 Gödel theorems correct?
- No. When von Plato put the 663 results into Coq, about 400 were verified as stated and about 200 were repaired by making the statement more precise or adding an assumption. About 50 were false, which von Plato says is no surprise because Gödel sometimes marked his own notes 'falsch!' or 'schlecht!'.
