Loading page…
Jan von Plato says computer checks validated hundreds of extracted results. That does not settle how much of a reconstructed proof belongs to Gödel.
Listen to this story
After a University of Helsinki team supplied Claude with transcriptions of Kurt Gödel’s shorthand notebooks and related scholarship, the model produced a 650-page account within days, according to logician Jan von Plato. It surfaced 663 theorems and proof ideas, but these ranged from completed arguments to sketches and false starts; von Plato reported that about 400 checked as stated, about 200 needed repairs, and about 50 were false. A Coq-checked reconstruction also leaves open how much of the proof belongs to Gödel and how much to Claude.
The project has studied 16 notebooks, comprising 1,009 pages written in Gabelsberger shorthand, since 2017.
Claude worked from researcher-prepared transcriptions and scholarship, not directly from images of the shorthand.
Von Plato said Claude’s reconstructed proof concerning the axiom of choice passed Coq checks, while its historical authorship remains unsettled.
Kurt Gödel’s unpublished notebooks may contain a much larger mathematical legacy than scholars understood. In findings described by the Guardian on November 13, logician Jan von Plato said Claude surfaced 663 theorems and proof ideas. Hundreds survived computer checks, he said—but a reconstructed proof has also raised a harder question: whose mathematical achievement does it represent?
Von Plato has led a University of Helsinki project studying 16 of Gödel’s workbooks since 2017. Written in the early 1940s, they span 1,009 densely written pages, much of them in an obsolete German shorthand called Gabelsberger. Understanding the mathematics had been painfully slow: the team was advancing at about one page a week before bringing Claude into the work.
The change came in September. Von Plato supplied Claude with his transcriptions, six books he had written on Gödel, and other scholarly literature. The model was therefore working from a researcher-prepared text and supporting scholarship, rather than simply deciphering images of shorthand. Within a couple of days, he said, it produced a 650-page explanation of the workbooks.
That explanation still needed checking page by page. Von Plato described the advantage as connecting material across the entire archive, rather than reading each page in isolation. Humans, he said, struggle to keep all the parts in mind. His claim was not that scholarly review had disappeared, but that Claude could assemble connections at a scale difficult for readers to retain.
Von Plato asked Claude to extract every theorem for which Gödel had a proof, a sketch, or an idea for a proof. That broad instruction produced the tally of 663. It combined different stages of mathematical work, not just completed arguments. Von Plato then reported checks using Coq, a proof assistant that verifies mathematical reasoning.
Von Plato said about 400 results were verified as stated using Coq.
About 200 needed repairs, such as more precise statements or added assumptions, he said.
Von Plato said about 50 were false.
The repairs were substantive qualifications: a theorem might need a sharper statement or another assumption before it held. False starts were also part of Gödel’s own working process. Von Plato noted that Gödel sometimes revisited his pages and added the marginal judgments falsch, meaning incorrect, or schlecht, meaning bad.
One reconstruction concerns the independence of the axiom of choice: whether that mathematical statement can be proved or disproved within the system under consideration. Von Plato’s first task for Claude was to determine whether Gödel’s notebooks contained such a proof. His assessment was that Gödel had come close, but had one definition wrong.
According to von Plato, Gödel had used the correct definition two years earlier. He believes Gödel would have reached it again with further work. Von Plato said the reconstructed proof Claude presented passed Coq’s checks. That is his reported validation of the reconstruction, alongside his interpretation of the unfinished notes.
Joel David Hamkins, a University of Notre Dame logic professor, offered a narrower historical reading. He had not seen the reconstruction, but said that if it held up, it would be remarkable and historically interesting. Material resembling Paul Cohen’s later proof, he cautioned, would show Gödel was on the path—not establish that he already possessed the proof.
“Although how much is Claude and how much is Gödel is a job for the historians,” Hamkins said. The reconstruction’s mathematical validity and its historical authorship remain separate questions.
Loading discussion...
Join the conversation
Explain where you draw the line between recovering an idea and finishing it.
Be the first to share a perspective or an experience.
Reader comments
Newest comments first. Replies stay oldest first.