Accelerating Historical Decryption
Logician Jan von Plato from Helsinki University spent years manually translating 1,009 pages of mathematical workbooks written by Kurt Gödel in the early 1940s. The dense texts were written in Gabelsberger shorthand, an obsolete German script known to only six scholars worldwide. Working by hand, von Plato digested roughly one page per week while managing a €2.5m European Research Council grant.
As reported via Hacker News, von Plato accelerated the project after consulting computer scientists and enlisting Anthropic's AI model, Claude. After being fed transcriptions, secondary literature, and von Plato's previously published books on Gödel, Claude produced a 650-page breakdown of the workbooks in two days. The AI cross-referenced patterns across the entire thousand-page archive simultaneously, a task impossible for human memory alone.
Verification and Uncovered Logic Themes
Von Plato tasked Claude with extracting all theorems for which Gödel had written, sketched, or conceptualized a proof, yielding 663 distinct items. To test the validity of the results, von Plato ran the AI-reconstructed proofs through Coq, an automated proof assistant program. Coq verified approximately 400 theorems as stated, while another 200 were successfully repaired with minor adjustments to assumptions or precision. Only about 50 were false, matching instances where Gödel himself had written marginal notes indicating errors.
The analysis resolved long-standing questions about Gödel's work on set theory, proving he was a single definition away from demonstrating the independence of the axiom of choice decades before Paul Cohen won the Fields Medal for the proof in 1966. Claude also identified 14 logical themes in the notebooks that scholars have never pursued in the 80 years since they were recorded. Researchers now plan to apply similar AI processing to Gödel's unexamined notebooks on physics and cosmology.
