Gödel's notebooks: Claude found 663 theorems in them

On November 13, the Guardian reported how Jan von Plato, a Finnish logician at the University of Helsinki, used the Claude model to analyze Kurt Gödel’s notebooks from the early 1940s. According to von Plato, Claude took a few days to produce a commentary on all 1,009 pages and picked out 663 theorems in them, hundreds of which nobody had known about.

What are Gödel’s notebooks?

After the incompleteness theorems of 1931, Gödel published only a handful of papers, but he left behind tens of thousands of manuscript pages. Among them are 16 notebooks from the early 1940s (the “workbooks”), 1,009 densely written pages of mathematics and logic in all. Gödel wrote much of it in Gabelsberger shorthand, a German system that was already obsolete when he took it up.

Von Plato has been working on the notebooks since 2017. He received €2.5 million for the project from the European Research Council (ERC), taught himself Gabelsberger shorthand and put together a small team. Working out the mathematical content went at roughly one page a week. At 1,009 pages, that comes to close to twenty years of work.

What did Claude do?

In August, at a conference in France on AI and theorem proving, computer scientists suggested to von Plato that he try Claude. In September he gave the model his transcriptions of the notebooks, six of his own books on Gödel and other scholarly literature.

So Claude did not read the shorthand. It worked on text that people had already transcribed, and its job was the part that had been going slowest: working out what those notes amount to mathematically.

A few days later von Plato had a 650-page explanation of the whole thing. He says it had to be checked page by page, but that a human cannot do this kind of work: you read one page, you forget, and 50 pages take you a year. The model, by contrast, sees everything at once (“It can see all of Gödel’s writings as one piece”).

Von Plato then asked for a list of every theorem for which Gödel had a proof, a proof sketch or an idea for a proof. Claude found 663. The results went into Coq, a program that checks whether mathematical proofs are correct:

1. about 400 theorems passed verification as written,
2. about 200 had to be “fixed”, meaning the statement was tightened or an assumption was added,
3. about 50 turned out to be false.

Von Plato explains the false ones by pointing out that Gödel, rereading his own notes, would sometimes write “falsch!” or “schlecht!” in the margin himself.

According to him, the notebooks contain dozens of results that the world only learned of in the 1970s and 1980s, and 14 lines of work in logic that nobody has picked up so far.

Did Gödel get there before Cohen?

In 1966 the American mathematician Paul Cohen was awarded the Fields Medal for showing the independence of the continuum hypothesis and the axiom of choice. Gödel’s response was that he had proved this result back in the 1940s. When colleagues asked for the proof, he could not reconstruct it from his notes.

The first task Claude was given concerned exactly this: do the notebooks contain a proof of the independence of the axiom of choice? The answer was “yes, almost”. According to von Plato, Gödel was one step short because he used a wrong definition, even though he had had the right one two years earlier. Claude presented a reconstructed proof, von Plato checked it in Coq, and the proof passed verification.

Joel David Hamkins, a professor of logic at the University of Notre Dame, has not seen the reconstruction and is more cautious. If the proof holds up, he thinks it will be remarkable and historically interesting, but notes that contain something resembling Cohen’s proof do not mean Gödel had that proof, only that he was on the right track. He added that “how much is Claude and how much is Gödel is a job for the historians”.

What should you keep in mind?

First, the source. All the numbers come from von Plato’s conversation with a journalist. The article links to no paper, no list of theorems and no Coq files, so for now there is little anyone can check independently.

Second, the 200 “fixed” theorems. If the statement had to be tightened or an assumption added, Hamkins’s question comes back for each of them: is this still Gödel’s result? The same goes for the reconstructed proof of the independence of the axiom of choice, given that in the notebooks from this period Gödel used the wrong definition.

Third, what Coq actually confirms. The program checks that a proof is correct. It does not settle whether Gödel had that proof, or whether the theorem written in Coq is the one Gödel meant. That is a judgment for people who know the manuscripts.

Is this something new in AI?

In October I wrote about the OpenAI paper claiming a model had refuted the exponential time hypothesis and about the formal verification of 123 libraries with Claude, and a few days ago about AlphaProof Code. In all of those cases the models were writing new proofs.

Here the model reads someone else’s mathematics from more than 80 years ago and looks for connections across a thousand pages that no person can hold in their head at once. The division of labor is the same, though: the model proposes, the proof checker verifies, and a human decides what follows from it. And there are more unread archives out there (Gödel alone left tens of thousands of pages).

FAQ

Which version of Claude analyzed Gödel’s notebooks?

We don’t know. The article only mentions the AI model Claude, with no version and no word on which product von Plato used.

What happens next with Gödel’s manuscripts?

Von Plato plans further research into those fourteen new lines of work in logic, and once his current projects are finished he wants to turn to Gödel’s notebooks on physics and cosmology, which he calls unknown territory.