Since 2017, the Finnish logician Jan von Plato has led a University of Helsinki project to understand 16 notebooks that Kurt Gödel filled in the early 1940s. His team understood the mathematics at about a page a week. In September, von Plato gave his transcriptions of the notebooks to Claude, Anthropic’s AI model. Within a couple of days, he had a 650-page explanation of all 1,009 pages, he told the Guardian in an interview published November 13, 2026.
He then asked Claude to list every theorem for which Gödel had a proof, a sketched proof or an idea for one. Claude found 663. They were put into Coq, a program that checks proofs one logical step at a time. About 400 held exactly as stated, about 200 had to be repaired and about 50 were false, according to von Plato.
The Guardian cites no paper, preprint or Coq files, and none had been made public as of November 14.
Joel David Hamkins, a logic professor at the University of Notre Dame, has not seen Claude’s reconstruction of a Gödel proof on the axiom of choice, a basic assumption about infinite collections. He told the Guardian that if it stands up, “it is remarkable and historically interesting.” He added: “how much is Claude and how much is Gödel is a job for the historians.”
A page a week in an obsolete shorthand
Gödel published his two incompleteness theorems in 1931. They showed that any system of rules free of contradictions and strong enough for ordinary arithmetic contains statements it can neither prove nor disprove. He left Austria in 1940, settled in Princeton and died in 1978. After the 1930s he published little, and his unpublished papers run to tens of thousands of pages, the Guardian reports.
The 16 notebooks, known as the Arbeitshefte, German for workbooks, are written largely in Gabelsberger, a German shorthand that was already obsolete when Gödel used it. The European Commission’s research database, CORDIS, calls the script “a true enigma.” Von Plato taught himself to read it and says he is “one of only six people who can read it in the world.” The European Research Council gave the project about 2.1 million euros from 2018 to 2024, according to CORDIS.
“Humans read one page at a time and we tend to forget things,” von Plato told the Guardian. “It takes us a year to read about 50 pages.”
A 650-page digest in a couple of days
In August, at a conference in France on AI and theorem proving, computer scientists suggested he try Claude. He gave Claude his transcriptions of the notebooks, other scholarly literature and six books he had written on Gödel. The Guardian lists no shorthand pages among these inputs. It does not say which version of Claude he used.
“In a couple of days, I got to see a 650-page explanation of the workbooks,” he said. “It had to be controlled page for page, but it’s basically a work that is impossible to do for human beings.” He credits the model’s memory: “The AI can connect all the pieces in a thousand pages.”
At a page a week, 1,009 pages would take about 19 years. That figure and the couple of days measure different jobs: a specialist’s full understanding, and a first pass that had to be checked page by page.
The axiom of choice, then 663 theorems
Von Plato’s first question for Claude involved set theory, the foundation of most mathematics. In 1966, Paul Cohen won the Fields Medal, the top prize in mathematics, for showing that two statements can be neither proved nor disproved from set theory’s standard rules. One is the axiom of choice; the other, the continuum hypothesis, is a claim about the sizes of infinite sets.
According to the Guardian, Gödel said he had proved the result in the 1940s. When colleagues asked, he could not reconstruct the proof from his notes. Von Plato asked Claude whether the notebooks held such a proof for the axiom of choice. The answer, the Guardian writes, was “yes, almost.”
“He was just one step away,” von Plato said. “There’s one definition that Gödel got wrong, but he had the right definition two years earlier.” Von Plato ran Claude’s reconstruction of the proof through Coq, and it passed.
The Helsinki group had pointed to this result before Claude. Its project page describes the work as of 2019 and lists “his 1942 proof of independence of the axiom of choice” among the results the team partly expected to find.
Of the 663 theorems Claude found, “about 400 were verified as stated, about 200 were repaired, meaning that perhaps the statement of the theorem had to be made more precise, or some assumption had to be added,” von Plato said. “About 50 were false, and this is no wonder.” Gödel sometimes wrote “falsch!” (wrong) in the margins of his notes.
Coq is now called the Rocq Prover. Anthropic used it in October, when Claude wrote machine-checked no-crash proofs across 123 open-source libraries.
Von Plato says the notebooks also contain “dozens of anticipations of results not known until the 70s and 80s” and “14 themes in logic that have not been pursued.” He plans to turn to Gödel’s physics and cosmology notebooks once he finishes his current logic projects.
Proof checkers behind other AI results this year
Another Gödel result went through a proof checker with Claude earlier this year. On June 1, Thierry Coquand, a computer science professor at the University of Gothenburg, posted a paper on arXiv, a public archive of papers. It describes a proof of Gödel’s second incompleteness theorem, which says that a consistent system strong enough for arithmetic cannot prove its own consistency. The proof, written in Agda, another proof checker, runs to about 50,000 lines with no unproven assumptions.
All of it came from conversation with Claude. “The author did not write any Agda code,” the abstract says. A first attempt failed because it rested on a false lemma, or supporting result, taken from an older paper. Claude ended up proving a statement that only resembled Gödel’s theorem.
On November 10, Google DeepMind said its AI agents had proved key security properties of the Signal protocol’s compiled code. The Signal protocol is the encryption behind the Signal messaging app, and compiled code is what a computer runs. The work took four weeks, and the agents wrote over six million lines of Lean, another proof checker.
DeepMind says such a job has historically taken expert teams years. WIRED reported, in a story republished by Ars Technica, that the work was a proof of concept, a limited demonstration that did not cover the whole Signal app.
Two other recent projects also used Lean. In October, the startup Axiom used AI agents to turn a 15,000-page proof into Lean code in 24 days. On November 10, a panel chaired by a Nobel laureate backed an AI-produced physics proof and relied on Lean’s checks to do it.
The figures rest on one interview
Every figure about the AI work comes from one interview. Von Plato has not released the 650-page digest, the theorem list or the Coq files, so nobody outside his group can check them. The three Coq counts are rounded and add up to 650, 13 short of 663. The interview does not say what became of the rest.
The Guardian does not say whether von Plato or Claude wrote the formal versions, meaning the statements as rewritten for Coq. That step counts, because a proof checker confirms only that a proof matches its formal statement. Coquand’s failed first attempt with Agda showed that a model “may reason correctly from an incorrect formal specification.”
Credit is another open question. On the axiom of choice, Hamkins told the Guardian: “The fact that there are things in there that resemble [Cohen’s proof] does not mean he had it. It shows he was on the path. You don’t get credit for work you don’t tell anyone about.”
Before Claude, the project had published in journals, among them a September 2025 paper by von Plato and Akihiro Kanamori in History and Philosophy of Logic. It covers Gödel’s first proof that the axiom of choice is consistent with set theory’s other rules.
What it means
For nine years, the limit on Gödel’s notebooks was reading. A handful of people could read the shorthand, and the mathematics came at about a week per page. If von Plato’s account holds, an AI model can now do a first full pass in a couple of days. A proof checker then tests the claims one by one.
The bottleneck moves to later steps. Someone has to state each theorem precisely, check the 650 pages against the source and decide whose idea a result was. In von Plato’s figures, about 200 of the 663 claims, roughly 30 percent, needed repairs.
The 1,009 workbook pages are a small part of Gödel’s unpublished papers. The next things to watch are whether von Plato releases the Coq files and the theorem list, whether historians accept the axiom of choice reconstruction and what the physics and cosmology notebooks hold.
Sources
- ‘Ahead of his time’: AI helps unlock discoveries hidden in notebooks of man who transformed maths, Alex Bellos, The Guardian, November 13, 2026
- The Gödel Enigma: Unveiling a Hidden Logical Heritage (GODELIANA), ERC Advanced Grant 787758, CORDIS, European Commission, read November 14, 2026
- Project description, Gödel Enigma research group, University of Helsinki, read November 14, 2026
- Auto formalisation of Goedel’s Second Incompleteness Theorem in Binary Recursive Arithmetic, Thierry Coquand, arXiv, June 1, 2026 (revised June 2, 2026)
- Introducing AlphaProof Code: a breakthrough in verifying complex software at depth, Pushmeet Kohli and Swarat Chaudhuri, Google DeepMind, November 10, 2026
- Google DeepMind just mathematically verified key parts of Signal, Lily Hay Newman (WIRED), Ars Technica, November 11, 2026
Header image: chart by MACCUS, data from Jan von Plato, interviewed by The Guardian, November 13, 2026
