Claire AI Digs Through Gödel's Notebooks: 663 Unknown Theorems Found

An AI model has uncovered hundreds of previously unknown theorems by Kurt Gödel, the Austrian logician whose incompleteness theorems of 1931 transformed mathematics. In a matter of days, Claude — the AI model built by Anthropic — produced a comprehensive digest of 1,009 pages of Gödel's unpublished notebooks, a corpus that human researchers had been decoding at roughly one page per week.

The most famous logician of modern times had, it turns out, discovered significantly more than anyone had thought.

"I was flabbergasted," said Jan von Plato, the Finnish logician at Helsinki University who has led the project to decipher Gödel's workbooks since 2017. "The workbooks not only contain dozens of anticipations of results not known until the 70s and 80s, but they also contain 14 themes in logic that have not been pursued. Gödel was far ahead of his time."

Why Gödel's notebooks matter

Gödel's two incompleteness theorems, published in 1931, demonstrated that in all mathematical systems there exist true statements that can neither be proved nor disproved. The result punctured the ambitions of earlier logicians who had hoped all mathematical truths were verifiable. It also inspired Alan Turing's 1936 paper, which founded the theory of modern computation — the intellectual bedrock of the digital age, and by extension of the very AI tools now reading Gödel's papers.

After his seminal results of the 1930s, Gödel published only a few papers. His unpublished material runs to tens of thousands of pages and is of intense interest to historians of science. The 16 notebooks at the center of von Plato's project, written in the early 1940s, are dense with mathematics and logic. Much of the text uses Gabelsberger, a German shorthand that was already obsolete when Gödel wrote in it.

A retirement project accelerated by AI

Von Plato began the project in 2017 as he faced mandatory retirement from Helsinki University. "What should I do to make myself indispensable? Oh yes, I'll start reading Gödel's enigmatic shorthand pages!" he said. He secured a €2.5m (£2.1m) grant from the European Research Council, taught himself Gabelsberger — "I am one of only six people who can read it in the world" — and assembled a small team.

Progress was slow. Human readers managed about 50 pages a year. The turning point came in August, at a conference in France on AI and theorem proving, where computer scientists suggested he enlist Claude. Back in Helsinki, von Plato fed the model his transcriptions of the workbooks, along with six books he had previously written on Gödel and other secondary scientific literature.

"In a couple of days, I got to see a 650-page explanation of the workbooks. It had to be controlled page for page, but it's basically a work that is impossible to do for human beings," von Plato said. "Humans read one page at a time and we tend to forget things. It takes us a year to read about 50 pages. We just are not able to keep in mind all the different parts."

The advantage is synthetic, not just speed. "The AI can connect all the pieces in a thousand pages. It can see all of Gödel's writings as one piece."