Claude Gödel Notebooks: 663 Theorems, 50 False

Jan von Plato says he was “flabbergasted.” The Finnish logician has spent nine years on Kurt Gödel’s workbooks, 16 notebooks and 1,009 pages from the early 1940s, and in September he handed his transcriptions to Claude. The Guardian reported on November 13 that a 650-page explanation came back within a couple of days.

That’s the headline. The numbers under it are more interesting, and they come from a proof checker, not from Claude.

Nine years at a page a week

Von Plato started the project at the University of Helsinki in 2017, as he faced mandatory retirement, according to the Guardian. He won a €2.5 million grant from the European Research Council and taught himself Gabelsberger, the German shorthand Gödel used. It was already obsolete when Gödel wrote in it. Von Plato told the paper he is “one of only six people who can read it in the world.”

Even so, progress ran at a page a week. The idea to try Claude came in August, at a conference in France on AI and theorem proving.

One detail matters for how much credit the model gets. Claude didn’t read the shorthand. Von Plato fed it his own transcriptions, plus six books he’d written on Gödel and other scientific literature on the subject. The model digested nine years of human decoding work. It didn’t replace it.

The one number: 663

Von Plato asked Claude to extract every theorem for which Gödel had a proof, a sketch of one, or an idea for one. Claude returned 663. Then von Plato ran them through Coq, a proof assistant that checks mathematics mechanically. His account to the Guardian:

Result in Coq	Roughly how many
Verified as stated	400
Repaired (statement made more precise, or an assumption added)	200
False	50

Those are von Plato’s rounded figures, so they don’t add up to exactly 663. Taking them at face value, around 60% of the list held as written, about a third needed fixing, and about 7% were wrong. Anyone who skipped the Coq step would have published about 50 false theorems.

Gödel isn’t a perfect benchmark either. Von Plato noted the false ones are “no wonder,” since Gödel himself sometimes wrote “falsch!” or “schlecht!” in the margins when rereading his notes. Some of those 50 may be Gödel’s mistakes that Claude faithfully extracted, not Claude’s own errors. The Guardian piece doesn’t split them out, and neither does anything else I could find.

A claim from 1966

The first question von Plato put to Claude was whether the notebooks contain a proof of the independence of the axiom of choice. Paul Cohen won the 1966 Fields Medal for that result, and Gödel claimed in 1966 that he had proved it himself in the 1940s. The answer, per von Plato: yes, almost. Gödel was “just one step away.” One definition was wrong, though he’d written the right one two years earlier. The Institute for Advanced Study, where Gödel worked from 1933 until his death in 1978, repeated the account on its own site. Von Plato said the reconstructed proof passed Coq.

He also says the notebooks hold “dozens of anticipations” of results not known until the 1970s and 80s, and 14 themes in logic nobody has pursued. Those two claims come from von Plato alone, and I haven’t seen an independent logician confirm them yet.

My read

My read: the useful pattern here is the pipeline, not the model. A human supplied clean input, Claude produced a big structured candidate list, and a formal verifier decided which items survived. Von Plato still checked the 650-page explanation page by page, he told the Guardian. If you swapped the Coq step for “trust the summary,” the story would be a lot less impressive and a lot less safe.

I’d also separate “previously unknown theorems” from “previously unpublished.” Hundreds of verified statements is a real result for a scholar working through shorthand. Whether the mathematical community will find them new or important is a different question, and only more reading by other logicians answers it. Von Plato is also the person who wanted the project to succeed, which is worth keeping in mind with his quotes.

Math is a friendly place for this work. A checker exists. We covered a similar split on OpenAI’s 722 math papers with Lean proofs, where the open question was who could test the model behind the proofs. Here a mechanical checker did the verifying, which is a better starting point, though I can only go by von Plato’s account of its results. Von Plato says he plans to turn to Gödel’s physics and cosmology notebooks next.

Sources

Note on sources: I read the Guardian article’s text through search excerpts, not the full page, and the IAS page summarises the Guardian. All figures above are von Plato’s, as quoted by the Guardian.