AI helps unlock hundreds of unknown theorems in notebooks of mathematician Gödel

After the 1,009 pages left by Austrian logician Kurt Gödel were read with the help of artificial intelligence, researchers say the notebooks contain hundreds of proved theorems that no one knew about until now.

Gödel's two incompleteness theorems, published in 1931, transformed mathematics and helped pave the way for the digital age. After that work in the 1930s he published only a few papers, but his unpublished writing runs to tens of thousands of pages.

Finnish logician Jan von Plato at Helsinki University has led a project since 2017 on 16 notebooks Gödel wrote in the early 1940s. Much of the material, known as the workbooks, is written in the German Gabelsberger shorthand, which was already obsolete when Gödel was using it.

Von Plato said progress had been painfully slow, about a page a week, until September, when he enlisted the AI model Claude. Within a couple of days Claude provided a comprehensive digest of the entire material, revealing that Gödel had proved hundreds of theorems no one knew about.

Von Plato said: 'I was flabbergasted. 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.'

The team first asked whether the workbooks contained Gödel's proof of the independence of the axiom of choice. According to von Plato, the answer was almost yes — one definition was wrong, but Gödel had written the right definition two years earlier. The reconstructed proof was later run through the proof assistant Coq, which verified it.

The team extracted 663 theorems from the workbooks. Von Plato said about 400 were verified as stated in Coq, about 200 were repaired by making the statement more precise or adding an assumption, and about 50 were false — in some of which Gödel himself had written 'incorrect' or 'bad' in the margin.

Gödel fled Austria under the Nazis in 1940, settled in Princeton, New Jersey, and became a close friend of Albert Einstein at the Institute for Advanced Study. In his later years he refused to eat food not cooked by his wife, and died of starvation in 1978.

Von Plato said he is sure continued study of Gödel's manuscripts will reveal further treasures. The workbooks contain, according to Claude, more than a dozen themes in logic and the foundations of mathematics that have not been found in more than 80 years, and Gödel's physics and cosmology notebooks are another area he plans to explore.

Von Plato received a €2.5m grant from the European Research Council for the project. He taught himself Gabelsberger shorthand and says he is one of only six people in the world who can read it.