AI Decodes Gödel’s Shorthand Notebooks, Revealing 663 Hidden Theorems
Finnish logician Jan von Plato used Anthropic’s Claude to decode 1,009 pages of Kurt Gödel’s 1940s notebooks written in obsolete Gabelsberger shorthand. The AI identified 663 theorems, including a near-complete proof of the axiom of choice’s independence that Gödel claimed in 1966. Von Plato verified the results using the Coq proof assistant, confirming that Gödel had discovered far more than historians previously knew.