A University of Helsinki team has used Anthropic’s Claude to examine 1,009 pages of Kurt Gödel’s unpublished workbooks. Claude extracted 663 candidate theorems; project leader Jan von Plato says about 400 checked in the Coq proof assistant as stated, about 200 needed repairs, and about 50 were false. Those figures, reported by the Guardian on November 13, 2026, make this a concrete example of AI-assisted research with a subsequent mathematical check.
The result depended on years of human work before Claude entered the process. Gödel wrote much of the material in Gabelsberger, an obsolete German shorthand. Von Plato’s team supplied transcriptions, books he had written about Gödel, and other scholarly literature. Claude produced a roughly 650-page explanation within days, according to von Plato, but he said it still had to be checked against the source page by page.
One finding is historically striking: von Plato sees in the notebooks an attempt close to proving the independence of the axiom of choice, a result associated with Paul Cohen. The reported argument contains an incorrect definition. Its resemblance to Cohen’s work is a reason to study Gödel’s notes closely, not evidence that Gödel completed or communicated a valid proof.
Years of Transcription Came Before Claude
The University of Helsinki’s Gödel Enigma project description identifies the Arbeitshefte as 16 notebooks containing roughly 1,200 shorthand pages on logic and mathematics, mostly written between the mid-1930s and mid-1940s. The Guardian’s 1,009-page figure refers to the workbooks examined in this account; the project’s larger figure describes the notebook series. The available sources do not explain the difference page by page.
Gödel’s symbols and compressed prose pose two separate problems. A researcher first has to decipher what a page says, then determine what its mathematical argument means and how it relates to material elsewhere in the notebooks. The project’s description of its methods explicitly combines reading shorthand sources with formal logic and historical research. Its team description also identifies a specialist focused on transcription.
Von Plato began studying the notebooks in 2017, according to the Guardian. He told the newspaper that progress on their mathematical content had been around a page a week before the Claude-assisted work. That pace helps explain the appeal of a corpus-wide digest: a connection between two distant pages is easy to miss when understanding each page is itself a research task.
Claude was given the team’s transcriptions, alongside von Plato’s books and other secondary literature, the Guardian reports. This is an important distinction. The reported result is not evidence that a model independently read 1,009 pages of obsolete shorthand from manuscript images. Human experts had already made the material more accessible and supplied context for interpreting it.
A Fast Synthesis Still Needed Page-by-Page Control
Von Plato brought Claude into the project after an August conference discussion about AI and theorem proving, according to the Guardian. He said the model returned an approximately 650-page explanation of the workbooks in a couple of days. The useful capability here was synthesis: following topics and possible relationships across a corpus too large for one reader to hold in mind at once.
The speed did not turn the digest into an authoritative edition. “It had to be controlled page for page,” von Plato told the Guardian. Checking a claim against a notebook page matters because an AI summary can merge separate ideas, overlook a qualification or present an exploratory calculation as a finished theorem. Checking it against the supplied transcription matters too: a mistake introduced while deciphering shorthand could carry through an otherwise coherent summary.
My view is that the transcriptions are the pivotal detail in this story. They gave Claude a workable representation of difficult source material, while the researchers’ books gave it a map of the relevant scholarship. The model could then propose connections at a scale the team said was hard to manage manually. That interpretation follows from the documented inputs and output; it is not a claim that every proposed connection was correct.
The sources do not identify the Claude version, prompts or sequence used to process the pages. They also do not provide the full digest. Those missing details limit what another team could reproduce from this report alone, even though von Plato’s account gives a clear picture of the division of labor.
Coq Separated Candidate Theorems From Checked Results
Claude’s list of 663 candidate theorems was a research queue, not a list of 663 established discoveries. Von Plato gave the Guardian the following approximate outcomes from checking the extracted claims with Coq:
- About 400 verified as stated.
- About 200 required repairs.
- About 50 were false.
The rounded categories add up to about 650, not exactly 663. The report does not give a full item-by-item accounting, so the difference should not be treated as a newly identified category of results. Nor do the figures provide a general accuracy score for Claude: this was a particular set of claims extracted from a particular corpus with expert-supplied context.
Coq checks formal proofs against precisely stated definitions and assumptions. In practical terms, an informal claim from a notebook has to be expressed in a form the proof assistant can handle, with enough proof steps for its checker to accept. A successful check is strong evidence for the formalized statement under those assumptions. It does not, by itself, settle whether the formalization faithfully captures Gödel’s wording, whether Gödel had written every needed step, or how a passage should be dated and attributed.
The repair count is especially informative. A promising mathematical idea can fail when its statement is too broad, a definition is wrong or an argument needs an additional condition. Repairing a candidate may lead to a valid result, but it changes the question historians must ask: which parts are in Gödel’s manuscript, and which were supplied during modern reconstruction? The available report does not set out the repairs individually.
This is why the Coq stage is more consequential than the digest’s length. Claude helped identify claims worth examining; formal checking supplied a way to reject some and sharpen others. Human comparison with the manuscripts remains necessary on either side of that check. The full Coq artifacts and reconstructed arguments are not available for independent assessment in the cited sources, so the numerical outcomes here remain von Plato’s reported results.
The Axiom of Choice Claim Has a Historical Limit
The axiom of choice says, roughly, that one can select an element from each set in a collection of nonempty sets. Proving its independence from a specified set of other axioms is a different task from proving the axiom itself: it involves showing that those axioms do not settle the choice question, subject to the relevant consistency conditions.
Cohen received a Fields Medal in 1966 for work establishing independence results concerning the axiom of choice and the continuum hypothesis, as the Guardian recounts. The newspaper also reports that Gödel later said he had proved the relevant result in the 1940s but could not reconstruct a proof for colleagues from his notes.
Frequently Asked Questions
3 questions
1Did Claude read Gödel’s shorthand directly?
The Guardian reports that the team supplied transcriptions and scholarly material. Its account does not establish that Claude independently deciphered the manuscript images.
