Claude read Gödel's shorthand notebooks. Coq threw out 50 theorems
One page a week. That was the pace Helsinki logician Jan von Plato managed through Kurt Gödel's early-1940s workbooks, 16 notebooks written in Gabelsberger shorthand that maybe six living people can read. Von Plato has worked on them since 2017 on a €2.5M ERC grant. In September von Plato handed Claude the transcriptions plus six of von Plato's own books and the secondary literature, and in a couple of days got back a 650-page explanation that von Plato says was checked page by page. The Guardian has the story: https://www.theguardian.com/science/2026/nov/13/kurt-godel-notebooks-ai-helps-unlock-hidden-discoveries-man-who-transformed-maths
The headline find is a nearly complete proof of the independence of the axiom of choice, one of the big open threads of that era. One definition in it was wrong; the correct version turns up in a notebook two years earlier. Von Plato ran the reconstruction through the Coq proof assistant and it passed. Then came the bigger ask: list every theorem Gödel proved, sketched or had an idea for. Claude found 663. In Coq, about 400 checked out as stated, about 200 needed repair, a sharper statement or an added assumption, and about 50 were false. Claude also flagged more than a dozen themes in logic that Gödel never pursued.
Those numbers are von Plato's as reported by the Guardian. There is no paper yet. Joel David Hamkins at Notre Dame, who has not seen the reconstruction, put the caveat well: how much is Claude and how much is Gödel is a job for the historians, and you don't get credit for work you don't tell anyone about.
The part worth keeping is the 50. A model that reads shorthand and archives at superhuman breadth will produce confident theorems, and roughly one in thirteen here was wrong. What made the project trustworthy was not the model; it was the human checking page by page and a proof checker that does not care how fluent the explanation sounds. Reading is now cheap. Verification is the expensive, valuable step, and in math it already has a machine.
Disclosure: clauday is written with Claude.
← Back to all articles
The headline find is a nearly complete proof of the independence of the axiom of choice, one of the big open threads of that era. One definition in it was wrong; the correct version turns up in a notebook two years earlier. Von Plato ran the reconstruction through the Coq proof assistant and it passed. Then came the bigger ask: list every theorem Gödel proved, sketched or had an idea for. Claude found 663. In Coq, about 400 checked out as stated, about 200 needed repair, a sharper statement or an added assumption, and about 50 were false. Claude also flagged more than a dozen themes in logic that Gödel never pursued.
Those numbers are von Plato's as reported by the Guardian. There is no paper yet. Joel David Hamkins at Notre Dame, who has not seen the reconstruction, put the caveat well: how much is Claude and how much is Gödel is a job for the historians, and you don't get credit for work you don't tell anyone about.
The part worth keeping is the 50. A model that reads shorthand and archives at superhuman breadth will produce confident theorems, and roughly one in thirteen here was wrong. What made the project trustworthy was not the model; it was the human checking page by page and a proof checker that does not care how fluent the explanation sounds. Reading is now cheap. Verification is the expensive, valuable step, and in math it already has a machine.
Disclosure: clauday is written with Claude.
Comments