Claude cracks Gödel's notebooks, finding hundreds of unknown theorems

What's going on

Kurt Gödel (1906–1978) is widely seen as one of the most original thinkers of the 20th century. His two incompleteness theorems of 1931 changed mathematics and paved the way for the theory of computation. After his groundbreaking work in the 1930s, Gödel published only a handful of papers. But his unpublished papers run to tens of thousands of pages.

As the Guardian reports, Finnish logician Jan von Plato of the University of Helsinki has now analyzed part of these papers with the help of Anthropic's AI model Claude. The material is a set of 16 notebooks Gödel wrote in the early 1940s, known as the "Workbooks": 1,009 densely written pages on mathematics and logic. According to von Plato, they contain hundreds of proven or sketched theorems that nobody knew about until now.

"I was stunned. The Workbooks contain not just dozens of anticipations of results that only became known in the '70s and '80s, but also 14 topics in logic that were never followed up. Gödel was far ahead of his time."

One page a week: the shorthand problem

The notebooks are hard to read. Gödel wrote most of them in Gabelsberger, a German shorthand that was already outdated in his day. Von Plato started the project in 2017, shortly before his mandatory retirement. Only half joking, he says he wanted to make himself indispensable. The European Research Council funded the project with €2.5 million. Von Plato taught himself the shorthand and says he is "one of only six people in the world who can read it." He also put together a small team.

Reading the notes was one thing. Understanding the mathematics was another, and that went very slowly, at about one page a week. The push toward AI came from computer scientists von Plato met in August at a conference in France on AI and automated theorem proving. Back in Helsinki, he gave Claude his own transcriptions of the Workbooks, along with six books he had written about Gödel and other specialist literature. So the AI didn't decipher the shorthand originals. It worked from transcriptions that humans had produced.

650 pages in a few days

Within a few days, von Plato had a 650-page commentary on the entire set of notebooks. He stresses that he had to check it page by page. Still, he says this is work that is practically impossible for humans:

"Humans read one page after another and forget things along the way. We need a year for about 50 pages. The AI can connect all the pieces across a thousand pages. It sees Gödel's writings as a whole."

Tasks like this play to a real strength of the technology. Large language models can keep very long texts in view at once and spot links between passages that are far apart. A human reader would need to take painstaking notes to do the same.

The nearly finished proof on the axiom of choice

Von Plato's first question to Claude had a historical background. Gödel's incompleteness theorems show that any sufficiently powerful mathematical system contains true statements that can be neither proved nor disproved within that system. Such statements are called "independent." In 1966, the American mathematician Paul Cohen received the Fields Medal, the highest honor in mathematics. He had shown that two famous statements of set theory are independent: the continuum hypothesis and the axiom of choice. The axiom of choice is the principle that from any collection of nonempty sets, you can always pick one element from each set.

At the time, Gödel said he had already proved this in the 1940s. But when colleagues asked him for the proof, he couldn't reconstruct it from his notes. So von Plato wanted to know whether the Workbooks contained such a proof. The answer: almost.

"He was just one step away. There's one definition Gödel got wrong, but two years earlier he had the right one. So he probably would have gotten there if he had kept going for a few more months."

Von Plato ran the reconstructed proof through Coq. Coq is a proof assistant, a program that mechanically checks every logical step of a proof. The proof passed. Von Plato believes Gödel could have won the 1950 Fields Medal if he had published it. The Guardian actually says "1940," but the medal wasn't awarded that year because of the war, so it's unclear which award is meant. Perhaps Gödel felt he had missed out on something when Cohen was honored, von Plato says. Above all, he praises Gödel's way of working. Gödel didn't play around with formulas and hope for a result, he says. He started from clear ideas and worked through them methodically.

663 theorems, machine-checked

Next, von Plato had Claude pull out every theorem for which Gödel had written down a proof, a proof sketch or at least an idea for a proof. The AI found 663. These were also checked in Coq:

Von Plato isn't surprised that about 50 theorems are false. When rereading his notes, Gödel himself sometimes wrote "wrong!" or "bad!" in the margin. According to Claude's analysis, the Workbooks also contain more than a dozen topics in logic and the foundations of mathematics that nobody has taken up in the more than 80 years since they were written. Next, von Plato plans to tackle Gödel's notebooks on physics and cosmology, which he calls "unknown territory."

Gödel: a genius with a tragic end

Gödel fled Austria and the Nazis in 1940 and settled in Princeton. At the Institute for Advanced Study, he became close friends with Albert Einstein. His incompleteness theorems were a blow to earlier logicians who had hoped that every mathematical truth could be proved. But they also gave the field a new direction and inspired Alan Turing's 1936 paper, which launched modern computability theory. In his later years, Gödel grew increasingly paranoid. He would eat only food his wife had cooked, and he died of malnutrition in 1978.

Our take

This story shows a sober but powerful use of language models in research. They don't solve open problems out of thin air. They open up huge, hard-to-access bodies of text and connect them. The workflow is what matters. An expert supplies the transcription and the background knowledge, the AI summarizes and reconstructs, and a formal tool like Coq checks the result at the end. That combination reduces the well-known risk of language models producing errors that sound plausible.

Some questions remain, though. So far, the results come only from von Plato's account in the Guardian. No peer-reviewed publication is mentioned. Joel David Hamkins, a professor of logic at the University of Notre Dame, hasn't seen the reconstruction yet. If it holds up, he says, it would be "remarkable and historically interesting." But he raises the key question: how much comes from Claude and how much from Gödel? That, he says, is "a job for the historians." If Claude filled a gap in Gödel's proof on its own, then the proof isn't entirely Gödel's.

Hamkins also urges caution about the credit:

"The fact that there are things in there resembling Cohen's proof doesn't mean Gödel had it. It shows he was on the way. You don't get credit for work you don't tell anyone about."

There's also a question of method. A Coq proof shows that the formalized statement is true. Whether the formalization captures exactly what Gödel meant is something a human has to judge. With the roughly 200 "repaired" theorems in particular, that comes down to interpretation. Still, if the numbers hold up, the AI did in days what would have taken a human team about twenty years at one page a week. That opens up archives that hardly anyone could read before.