Von Plato uses Claude to extract 663 theorems from Gödel notes

Before he brought in Claude in September, Jan von Plato had been decoding Kurt Gödel's 1,009-page shorthand notebooks at roughly one page per week. The Finnish logician had been working on them since 2017 at the University of Helsinki. Within days of handing the model his transcriptions and six of his own books on Gödel, Claude returned a 650-page explanation of the workbooks and a catalogue of 663 theorems the Austrian logician had proved, sketched or outlined in Gabelsberger, a German shorthand already obsolete in Gödel's own lifetime, the Guardian reports.

Von Plato then put the catalogue through Coq, a formal proof verifier. Roughly 400 theorems went through as stated. About 200 needed sharper statements or extra assumptions. Around 50 came out false, which fit a pattern Gödel himself set: pages are marked with his own marginal verdicts, 'falsch' (incorrect) and 'schlecht' (bad).

The headline find was a near-complete reconstruction of the independence of the axiom of choice, a result Gödel claimed in 1966 but never published. Paul Cohen later won the Fields Medal for the same result. Claude's version passed Coq.

"In a couple of days, I got to see a 650-page explanation of the workbooks," von Plato said. "It's basically a work that is impossible to do for human beings."

Joel David Hamkins of Notre Dame warned that disentangling "how much is Claude and how much is Gödel is a job for the historians." The notebooks also contain predictions of results that only became known in the 1970s and 1980s, plus 14 topics in logic that have still not been developed.

Anthropic has featured in 381 of our tracked stories over the past ninety days; this is one of the rarer entries where the use case is a Finnish logician reading an Austrian mathematician's shorthand rather than a commercial deployment.