The model read the transcription, not the shorthand
The shorthand is the part of this story most likely to be misread, so it is worth being plain about the division of labor. Gabelsberger defeated readers for decades because almost nobody alive reads it fluently. Von Plato does. He supplied his transcriptions of workbooks totaling 1,009 pages, much of them in shorthand, alongside six of his books and other secondary literature.
That does not shrink the result. Holding connections across a thousand pages at once, and returning a structured catalogue instead of a summary, is not work a single scholar can do in days at any level of shorthand fluency. Von Plato's own reaction, as quoted by the Guardian, was that he was "flabbergasted" and that the 650-page explanation is "basically a work that is impossible to do for human beings."
It does change what the result proves. This is evidence that a frontier model can do large-scale scholarly synthesis over a difficult, specialist corpus prepared by an expert. It is not evidence that a model can walk up to an undeciphered archive and read it.
The checker is the useful part of the story
Most AI-and-science stories stop at the model's output. This one has a second step, and the second step is where the numbers get honest.
Von Plato reports that Coq verification established about 400 of the 663 claims as stated. About 200 went through after repairs — the statement of the theorem made more precise, or an assumption added — which in logic can mean anything from a missing condition to a claim that was never quite what the notebook said. About 50, he says, were false.
Read together, the reported split describes a catalogue that is valuable and unfinished. On von Plato's rounded counts, roughly three in five entries survived the checker as stated — a serious research asset. A substantial share needed repair or failed, so the catalogue is not a finished edition of Gödel, and nobody should cite the 663 as if all of them were established results. The three rounded figures also sum to about 650 rather than 663, and the reporting provides no detailed breakdown. Until von Plato publishes the catalogue itself, that gap cannot be closed from the reporting.
One reconstruction, two separate questions
The axiom-of-choice reconstruction is the finding that will travel, and it carries two questions that should not be merged.
The first is mathematical: does the reconstructed argument hold? Von Plato says the version Claude produced passed Coq. A successful Coq check would establish the formalized claim under its stated assumptions. Without the statements, assumptions and proof artifacts, outside readers cannot assess whether the formalized version matches the mathematical claim being reported.
The second is historical: how much of that argument is Gödel's, and how much is the model completing a sketch in its own way? The reconstruction itself underlines the question: on von Plato's account, Gödel was one step away, with one definition wrong — though he had used the right definition two years earlier, which is why von Plato believes he would have arrived at it. Joel David Hamkins, a professor of logic at the University of Notre Dame, put the attribution problem directly in the Guardian's reporting: disentangling "how much is Claude and how much is Gödel is a job for the historians." Hamkins added that resemblance to Cohen's proof "does not mean he had it. It shows he was on the path." Hamkins has not seen the reconstruction. A reconstruction can be valid mathematics and still not be the proof Gödel had in mind. Coq can speak to the first question. It cannot settle the second.
There is also a limit on the first answer for now. The catalogue, the transcriptions as fed to the model, and the reconstruction have not been released, so no outside logician can rerun the check or inspect where the model filled a gap. That is normal for work reported before publication. It is still the difference between a reported result and a result the field can use.
What this is actually a test of
Strip away the famous name and the remaining claim is a practical one. An expert with a large, well-prepared, highly structured corpus got a 650-page synthesis back in days, and a formal checker then gave him a way to grade the output claim by claim. The account suggests a workflow worth investigating — expert-prepared source material, model-assisted synthesis, explicit verification — in fields like archives, case law and engineering records. It does not establish equivalent results in other fields.
The workflow's limits are in this story too. Where there is no von Plato, there is no clean corpus to hand over. Where there is no checker like Coq, there is no comparably direct way to find the false entries among the 663. The Gödel notebooks are close to a best case for this kind of work, and on the reported counts the output still needed repair roughly two times in five.
Sources
- [1] The Guardian, "'Ahead of his time': AI helps unlock discoveries hidden in notebooks of man who transformed maths", November 13, 2026 — original reporting; all figures are von Plato's account.
- [2] Institute for Advanced Study, "'Ahead of His Time': AI Helps Unlock Discoveries Hidden in Notebooks of Man Who Transformed Maths", November 13, 2026Read source
- [3] AI Weekly, "Helsinki team uses Claude to surface 663 Gödel theorems", November 13, 2026Read source