Claude Reads Gödel’s 1,009 Pages: About 400 Theorems Check Out, One Line Short of the Axiom of Choice

Finnish logician Jan von Plato gave Claude the English transcription of 16 workbooks Gödel kept after 1940, 1,009 pages in all. In a lecture at the University of Vienna he said Claude returned an interpretation that grew from 650 pages to 1,084, and listed 663 results that looked like theorems. After formal checks with Josef Urban and others, about 400 hold outright, about 200 are right in outline but need extra assumptions, 55 are wrong, and a few are still being checked.

People transcribed the shorthand. Claude read the English.

Gödel died in 1978 and left a large body of unpublished notes. His 1931 incompleteness theorems influenced Turing. The later notebooks were written in Gabelsberger shorthand, which very few people can read. Von Plato started the project in 2017, near mandatory retirement, and won a €2.5 million grant from the European Research Council. He has said that only about six people in the world can read the shorthand, and that he is one of them.

The target was the 16 workbooks Gödel wrote after settling in Princeton in 1940. Von Plato found that the AI systems of the time could not read the shorthand, so the transcription had to be done by hand. The team spent years turning the notes into modern English. Even then the writing is compressed and jumps quickly. A human pace of about one page a week meant roughly 50 pages a year. This summer, at a French meeting on AI and theorem proving, computer scientists suggested he try Claude. He then gave the model the 1,009-page transcription, six of his own monographs, and a set of modern logic papers. More model coverage is in AI news.

663 sketches, about 400 theorems that hold

Von Plato described Claude as a digital tool with a “Mozart-like” view: a person forgets page 10 by page 500, while the model can hold the notebooks and the related literature in one context. It first extracted 663 results with the shape of a theorem. Formal verification then split them into about 400 that are fully correct, about 200 whose core idea is right but needs assumptions, and 55 that are wrong. On that count, in the less than three years after Gödel reached the United States in the early 1940s, he was producing a new result about every two days.

The axiom of choice: the frame was there, one definition was wrong

The axiom of choice was long unsettled: can it be derived from the other basic axioms? In 1963 Paul Cohen proved its independence with forcing, and received the Fields Medal in 1966. At the ceremony Alonzo Church said publicly that Gödel had already, in 1942, proved the independence of the axiom of constructibility inside type theory and believed the argument could reach the axiom of choice, before his interests turned to philosophy. Cohen later wrote, in 2002, that Gödel admitted having a method but denied it was about type theory and would not show it. In a letter to W. Rautenberg on 30 June 1967, Gödel said he had only reached a partial result. Hao Wang wrote that Gödel regretted not finishing the work.

Claude’s reading is that, more than twenty years before Cohen, Gödel had already built an equivalent framework. He represented “possible worlds” as infinite strings of 0s and 1s, then used a diagonal argument to show that no such choice function exists in that setting. The gap was a definition. Reports say he wrote one wrong line in the key notion of finite support. Elsewhere in the notes he had written the correct definition, and forgot it when he returned to the pages in the 1960s. Von Plato sent the reconstructed proof to the Coq proof assistant, and it checked. He also sent the human-and-model paper to Gödel scholar Akihiro Kanamori. Kanamori did not know an AI had been involved, and called the piece sharp both mathematically and historically.

Quantum measurement and a closed loop of time

The same notebooks contain logical results that were rediscovered only in the 1970s and 1980s, including the independence of the axiom of constructibility and a strong-normalization proof in functional interpretation. Claude also listed 14 topics that still have little published work, and expanded them into an outline of about 50 pages.

The physics sits further back. In 1935 Einstein, Podolsky and Rosen published the EPR paper, asking whether quantum mechanics is complete. Reports say Podolsky had heard Gödel lecture on incompleteness the year before. Gödel had planned to work on quantum mechanics in 1935 and then turned to set theory. In the notes, Claude found calculations of how a coupled system changes after a measurement. The update is not von Neumann’s 1932 rule. It is the rule later named for Lüders, which Lüders published only in 1951.

In 1949 Gödel found a solution of Einstein’s field equations in which the universe rotates. Far enough from the axis, the light cones tip until time can close on itself. Claude’s reading is that this was not a joke. The notes include astronomical observations he searched, looking for a statistical tilt in how galaxies rotate that a Coriolis effect would produce. In 1978 Gödel died of starvation after refusing food that his wife had not prepared.

FAQ

Q: Did Claude read Gödel’s shorthand originals? A: No. Von Plato’s team spent years turning the Gabelsberger shorthand into modern English. Claude read that 1,009-page transcription, plus the professor’s books and modern papers.

Q: How many new theorems were actually proved? A: The detailed count in the reports is 663 theorem-shaped results. After formal checks, about 400 hold outright, about 200 are right in outline but need assumptions, 55 are wrong, and a few are still open. The round number “more than 440” is less precise than this split.

Q: Did Gödel prove the independence of the axiom of choice before Cohen? A: The framework Claude reconstructed is equivalent to Cohen’s later proof, but Gödel wrote one wrong line in the definition of finite support. The published proof is still Cohen’s, from 1963. The reconstruction has been checked in Coq.