Claude helps a Helsinki logician read Gödel's shorthand workbooks, turning up hundreds of theorems

The Guardian reports that Jan von Plato, who has led a Helsinki University project on Kurt Gödel's 16 early-1940s "workbooks" (1,009 pages, much of it in the obsolete Gabelsberger shorthand) since 2017, gave Claude his transcriptions, his earlier books on Gödel and the secondary literature in September. According to von Plato, Claude produced a 650-page explanation of the workbooks within a couple of days, which he says had to be checked page by page.

What von Plato says it found. Asked whether the workbooks contain a proof that the axiom of choice is independent, Claude reconstructed one that von Plato says is "almost" complete, with one wrong definition Gödel had right two years earlier. He says the reconstructed proof passed the Coq proof assistant. Asked to extract every theorem Gödel proved, sketched or had an idea for, Claude listed 663. Von Plato says about 400 were verified as stated in Coq, about 200 needed repair, and about 50 were false. He also says Claude identified more than a dozen logic themes that have not been pursued.

Caveats. Joel David Hamkins of Notre Dame, who had not seen the reconstruction, told the Guardian that if it stands up it is "remarkable and historically interesting", but that how much of it is Claude's and how much Gödel's is a question for historians, and that resembling Cohen's proof does not mean Gödel had it.