Helsinki team uses Claude to surface 663 Gödel theorems

Jan von Plato, a Finnish logician at the University of Helsinki, had been decoding Kurt Gödel's 1,009 pages of unpublished notebooks at roughly one page per week since 2017. In September he handed his transcriptions to Anthropic's Claude; within days it returned a 650-page analysis and a catalogue of 663 theorems Gödel had proved, sketched, or outlined in a notebook written in Gabelsberger, an obsolete German shorthand. "I was flabbergasted," von Plato told the Guardian.

Von Plato is, by his own account, "one of only six people who can read it in the world." His broader project, backed by a €2.5 million European Research Council grant, covers 16 workbooks Gödel wrote in the early 1940s.

Of Claude's 663 proposed theorems, about 400 were verified as stated via the Coq proof assistant, around 200 needed repair, and roughly 50 were false, a few of which Gödel himself had already marked "falsch" or "schlecht." "It had to be controlled page for page," von Plato said, "but it's basically a work that is impossible to do for human beings."

The most eye-catching finding concerns the independence of the axiom of choice, the problem Paul Cohen won the 1966 Fields Medal for cracking. The notebooks place Gödel, writing in the 1940s, "just one step away," having relied on a definition he had successfully altered two years earlier.

Joel David Hamkins, a logician at the University of Notre Dame, called the result "remarkable and historically interesting" but cautioned that "how much is Claude and how much is Gödel is a job for the historians." Von Plato says the workbooks contain "dozens of anticipations of results not known until the 70s and 80s" and "14 themes in logic that have not been pursued."