Claude lists 663 theorems in Gödel's shorthand notebooks, says the logician who transcribed them
Jan von Plato gave Claude his transcriptions. About 400 of the theorems checked out in Coq as stated. No outside logician has reviewed it.
The logician Jan von Plato of the University of Helsinki has spent since 2017 on 16 notebooks Kurt Gödel wrote in the early 1940s. They run to 1,009 pages, much of it in Gabelsberger, an obsolete German shorthand. Von Plato taught himself to read it and says he is one of six people who can. By hand he got through about a page a week.
He gave Claude his transcriptions of the notebooks, his six books on Gödel and other writing about him. Within a couple of days it returned a 650-page explanation of the notebooks and a list of 663 theorems for which Gödel had a proof, a sketch of one, or an idea for one. Von Plato checked the explanation page by page. In Coq checks (software that verifies proofs line by line), about 400 of the theorems held as Gödel stated them, about 200 held after he tightened the statement or added an assumption, and about 50 were false. He says Gödel sometimes wrote “falsch!” or “schlecht!” beside his own errors.
Von Plato also asked whether the notebooks held a proof that the axiom of choice cannot be settled from the other axioms of set theory, a result Paul Cohen won the 1966 Fields Medal for. Gödel claimed to have proved it in the 1940s but could not reconstruct it when pressed. Claude found an almost complete proof. One definition was wrong, and Gödel had written the right one two years earlier. The reconstructed proof passed Coq.
What it means
If the list holds up, AI shortened a decades-long reading job to days, and a proof checker caught the errors. Whether any of it is new mathematics is a separate matter: the theorems are Gödel’s, and the open question is how much of each one he had.
Caveats
- This is von Plato’s own account as reported by the press. We could not load the Guardian article and read it through two copies of its reporting, which differ on some details.
- No paper or data has been released, so nobody else can rerun the extraction. The coverage does not name the Claude model.
- Joel David Hamkins of Notre Dame had not seen the reconstruction. He called it “remarkable and historically interesting” if it holds, and said separating Claude’s part from Gödel’s “is a job for the historians”.
- Hamkins also said a resemblance to Cohen’s proof shows Gödel was on the path, not that he had the result. Von Plato’s view that Gödel would have won a Fields Medal is an opinion.
- A Coq check confirms the formal statement, not that Gödel held the proof. The coverage gives the counts of about 400, 200 and 50 without saying who ran the checks.