THE CRUNCH
Kurt Gödel's early 1940s workbooks, 1,009 pages of densely written maths and logic largely in the obsolete German shorthand Gabelsberger, have yielded hundreds of previously unknown proved theorems after a researcher turned to the AI model Claude. Jan von Plato of Helsinki University has led a project on the 16 notebooks since 2017, but progress ran at roughly a page a week. In September, after computer scientists at a conference on AI and theorem proving suggested the idea, he fed Claude his transcriptions plus six books he had written on Gödel. Within a couple of days the model produced a 650-page explanation of the whole material.
Von Plato said the output still had to be checked page by page, but described the task as impossible for humans, who read one page at a time and forget. "The AI can connect all the pieces in a thousand pages. It can see all of Gödel's writings as one piece," he said. He reported that the workbooks contain dozens of anticipations of results not known until the 1970s and 1980s, plus 14 themes in logic that were never pursued.
One early test concerned a long-standing puzzle. When Paul Cohen won the 1966 Fields medal for showing the independence of the continuum hypothesis and the axiom of choice, Gödel claimed he had already proved the latter result in the 1940s but could not reconstruct a proof from his notes when pressed. Von Plato asked Claude whether the workbooks held such a proof. The answer: almost. Gödel was one step away, using one wrong definition, though he had the right definition two years earlier.