AI helps unlock discoveries hidden in Kurt Gödel's notebooks

From the article:

Since 2017, the Finnish logician Jan von Plato has led a project at Helsinki University to understand the contents of 16 notebooks that Gödel wrote in the early 1940s. This material – the “workbooks” – is 1,009 pages of densely written text about maths and logic. Much of it is written in a German shorthand, Gabelsberger, that was obsolete even when Gödel was using it.

Progress in the mathematical understanding of the text was painfully slow – about a page a week – until September, when von Plato enlisted the help of the AI model Claude. Within a couple of days, Claude had provided a comprehensive digest of the entire material, revealing Gödel had proved hundreds of theorems that no one knew about.

[...]

In August, at a conference in France about AI and theorem proving, von Plato met computer scientists who suggested that he co-opt the help of Claude in trying to make sense of the workbooks. On his return to Helsinki he began the process, showing Claude his transcriptions of the workbooks, as well as 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,” he 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 AI can connect all the pieces in a thousand pages. It can see all of Gödel’s writings as one piece.”

[...]

Gödel reacted to Cohen’s Fields medal by saying that he had already proved the result in the 1940s. Yet when pushed for a proof by his peers, Gödel was unable to reconstruct one from his notes.

The first task von Plato set Claude was to discover if Gödel’s workbooks had a proof of the independence of the axiom of choice, which would reveal that Gödel had been telling the truth in 1966. The answer came back: yes, almost. “He was just one step away,” said von Plato. “There’s one definition that Gödel got wrong, but he had the right definition two years earlier, and so the thought is that he would have arrived at the right definition anyway if he had just continued for a few months. For me, the architecture of his proof is just wonderful. It makes all of these results of set theory follow a uniform pattern.

[...]

Von Plato said that when Claude presented him with the reconstructed proof of the independence of the axiom of choice, he ran it through the proof assistant Coq, a program that verifies the validity of mathematical proofs, and it passed. Von Plato believes that had Gödel published his work on the axiom of choice, he would have won the 1940 Fields medal. “Maybe he felt that when Cohen got the medal, that that was something he sort of missed.”

In further discussions with Claude, von Plato asked the AI model to extract all theorems in the workbooks for which Gödel either had a proof, had sketched a proof or had an idea for a proof. Claude found 663. When these results were put into Coq: “About 400 were verified as stated, about 200 were repaired, meaning that perhaps the statement of the theorem had to be made more precise, or some assumption had to be added. About 50 were false, and this is no wonder. Gödel himself, when rereading his notes, would occasionally add a marginal remark: falsch! [incorrect] or schlecht! [bad].”

[...]

Hamkins said: “The fact that there are things in there that resemble [Cohen’s proof] does not mean he had it. It shows he was on the path. You don’t get credit for work you don’t tell anyone about. But Gödel had so many ground-breaking ideas that it is maybe not surprising that his notebooks are full of exciting things.”