The Legacy of Kurt Gödel
Kurt Gödel, a prominent Austrian logician, was one of the most influential thinkers of the 20th century. His seminal work, particularly his two incompleteness theorems published in 1931, fundamentally altered the field of mathematics and laid crucial groundwork for the development of modern computing. Gödel’s initial research inspired figures like Alan Turing, ultimately helping pave the way for the digital age.
While Gödel produced a few published papers after his breakthrough results in the 1930s, his accumulated unpublished material spans tens of thousands of pages, making it of immense interest to historians of science.
Decoding Obsolete Shorthand
Beginning in 2017, Finnish logician Jan von Plato initiated a project at Helsinki University focused on interpreting sixteen notebooks written by Gödel during the early 1940s. This collection, referred to as “workbooks,” comprises 1,009 pages of dense mathematical and logical text. A significant challenge for the researchers was that much of the writing was done in Gabelsberger, a German shorthand method that had become obsolete even when Gödel utilized it.
Initially, progress in understanding the material was extremely slow, requiring approximately one page of decipherment each week. This changed dramatically in September when von Plato incorporated the artificial intelligence (AI) model, Claude, into the research. Within a short period, Claude provided a comprehensive summary of the entire body of work, revealing that Gödel had proven hundreds of theorems that had previously remained undiscovered.
Von Plato expressed his astonishment at the findings, noting that the workbooks contained not only dozens of results that anticipated discoveries not known until the 1970s and 1980s, but also featured 14 unique themes in logic that had not yet been explored. He remarked that Gödel was “far ahead of his time.”
Gödel’s Contributions to Logic and Computation
Gödel fundamentally changed the trajectory of logic by demonstrating the inherent limitations of formal mathematical knowledge. His incompleteness theorems established that within any formal mathematical system, there exist statements that can neither be proven nor disproven within that system. Although this result challenged previous generations of logicians who believed all truths were verifiable, Gödel’s work spurred the field forward, notably inspiring Alan Turing to write his 1936 paper that launched the theory of modern computation.
When Gödel fled Austria under the Nazis in 1940, he settled in Princeton, New Jersey, where he became a close friend of Albert Einstein at the Institute of Advanced Study. He eventually died of starvation in 1978.
AI’s Role in Verification and Discovery
Von Plato began his Gödel project in 2017 because he was facing mandatory retirement from Helsinki University. He stated that starting the effort allowed him to feel “indispensable.” He secured a €2.5 million grant from the European Research Council, taught himself Gabelsberger shorthand—making him one of only six people globally capable of reading it—and assembled a small team.
Following a conference in France on AI and theorem proving, von Plato sought assistance from computer scientists who recommended using Claude. After showing the AI his transcriptions and six books of secondary scientific literature on Gödel, he reported that Claude generated a 650-page explanation of the workbooks. He noted that this level of synthesis was impossible for human researchers, as humans process information one page at a time and tend to forget details over time.
Gödel’s incompleteness theorems showed that certain statements could not be proven or disproven within the system itself. This context is relevant because, in 1966, mathematician Paul Cohen won the Fields medal, the highest honor in mathematics, for demonstrating the independence of two established mathematical statements: the continuum hypothesis and the axiom of choice.
Gödel had previously stated that he had proven this result in the 1940s. When von Plato first tasked Claude with finding proof of the independence of the axiom of choice, the AI indicated that the proof was nearly complete. Von Plato explained that Gödel was “just one step away,” suggesting that a minor definitional error prevented its completion, but that the underlying conceptual architecture was flawless.
Upon receiving the reconstructed proof for the independence of the axiom of choice, von Plato ran it through Coq, a specialized program used to verify mathematical proofs, and it passed. Von Plato suggested that if Gödel had published this work, he would likely have received the 1940 Fields medal. He noted that Gödel’s approach was characterized by starting with clear ideas and following a methodical path, rather than merely manipulating formulas.
By directing Claude to extract all theorems from the workbooks for which Gödel had proof, a sketch, or an idea, the AI identified 663 such theorems. When these were entered into Coq, approximately 400 were verified as stated, 200 required minor adjustments to the statement or assumptions, and 50 were found to be incorrect, a finding von Plato attributed to Gödel’s own marginal corrections (such as *falsch!* or *schlecht!*).
Von Plato concluded that the study of these manuscripts is ongoing, anticipating that they hold more than a dozen themes in logic and the foundations of mathematics that have not been addressed in the over 80 years since they were written. Joel David Hamkins, a professor of logic at the University of Notre Dame, commented that while he has not seen the reconstruction, if the findings are accurate, they are “remarkable and historically interesting,” concluding that the notebooks are “full of exciting things” due to Gödel’s sheer volume of groundbreaking ideas.
