AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems

Kurt Gödel’s 16 workbooks, written in the 1940s, comprise 1,009 pages of mathematical notes, much of them in the obsolete German shorthand Gabelsberger. Finnish logician Jan von Plato and his team had spent years deciphering the material slowly. After feeding their transcriptions and related scholarship into the AI model Claude, von Plato received a detailed account of the notebooks within days. The analysis identified hundreds of results and more than a dozen research themes that appear to have been overlooked for over 80 years. The notebooks also include ideas anticipating developments in logic and mathematics decades later.

A key test was Gödel’s claim that he had proved the independence of the axiom of choice before Paul Cohen’s celebrated 1960s work. Claude reconstructed a proof that von Plato says came close but contained a faulty definition; the reconstructed argument nevertheless passed the Coq proof-checking system. Claude identified 663 theorem statements, sketches or proof ideas: about 400 were verified as written, roughly 200 needed corrections or added assumptions, and around 50 were false. Other logicians caution that resembling a later proof does not establish that Gödel completed or communicated it, and historians must distinguish Gödel’s contribution from the AI’s reconstruction. The findings suggest the notebooks may hold substantial new material, including unexplored work on logic, mathematics, physics and cosmology.