Source: The Guardian science report by Alex Bellos published November 13, 2026.
Since launching the transcription effort upon reaching mandatory retirement age at the University of Helsinki in 2017, Jan von Plato estimated his team took roughly a year to decode and analyze 50 workbook pages because human readers lose track of cross-references across a thousand dense pages. After computer scientists at an August conference in France suggested using Anthropic's Claude, von Plato supplied the AI with his transcribed shorthand pages alongside his own six books and secondary literature on Gödel.
The most dramatic historical test targeted Gödel's 1966 insistence that he had already proved the independence of the axiom of choice during the 1940s—before American mathematician Paul Cohen won a Fields Medal for proving both it and the continuum hypothesis independent of standard set theory. Claude found Gödel was 'just one step away,' stumbling over one flawed definition even though the correct formulation already sat in notes written two years earlier; once repaired, the architecture of Gödel's proof passed Coq.
Besides uncovering dozens of set-theory and proof-theory anticipations not published by other mathematicians until the 1970s and 1980s, Claude flagged more than a dozen logic themes that remain untouched 80 years later. Von Plato praised Gödel's structured progression from clear conceptual aims rather than blind formula manipulation.
Outside logicians urged historical caution about attribution boundaries. University of Notre Dame logic professor Joel David Hamkins, who had not yet reviewed the reconstructed proof directly, said that if Coq verification holds up it will be historically fascinating, while stressing that teasing apart Gödel's original insight from Claude's deductive scaffolding will require sustained scrutiny by mathematical historians.