Jan von Plato discovered that the AI model Claude identified 663 theorems within the 1,009 pages of handwritten workbooks by Kurt Godel. The logician at Helsinki University began his project in 2017 to study these 16 notebooks written in the early 1940s. Because the text uses Gabelsberger, an obsolete German shorthand, human progress on the mathematical understanding of the material moved at a rate of one page per week. After meeting computer scientists in France this August, von Plato provided Claude with his transcriptions and six books he wrote on Godel. Within two days, the AI produced a 650-page explanation of the material.
The AI connects the pieces
The speed of the AI provides the most impressive aspect of this discovery. While humans read one page at a time and forget details, the AI can see all of Godel’s writings as one piece. This capability revealed that Godel had dozens of anticipations of results not known until the 1970s and 1980s. Claude also found 14 themes in logic that have not been pursued in the 80-plus years since they were written.
When Claude extracted the theorems, it found 663 instances where Godel had a proof, a sketch, or an idea for a proof. Testing these results through the Coq proof assistant program yielded these specific outcomes:
| Result Category | Number of Theorems |
|---|---|
| Verified as stated | 400 |
| Repaired for precision | 200 |
| False | 50 |
Von Plato noted that Godel occasionally added marginal remarks like "falsch!" or "schlecht!" to his own notes.
A near miss for a Fields medal
The AI also reconstructed a proof regarding the independence of the axiom of choice. Godel claimed he had proved this result in the 1940s, but he could not reconstruct it for his peers when Paul Cohen won the Fields medal for it in 1966. Claude’s reconstruction passed the Coq verification, though it required correcting one definition that Godel had gotten wrong. Von Plato believes that if Godel had published this work, he would have won the 1940 Fields medal. Joel David Hampkins of the University of Notre Dame said that while the findings are historically interesting, determining how much belongs to Claude versus Godel remains a job for historians.
