Claude helped uncover unknown results in Kurt Gödel’s notebooks

Notebooks that resisted deciphering

Kurt Gödel was one of the most original thinkers of the 20th century. His two incompleteness theorems, published in 1931, changed mathematics and helped lay the groundwork for the digital age. They show that every mathematical system contains true statements that cannot be proved or disproved within that system. These results defined the limits of mathematical knowledge, but also opened up new areas of logic. In particular, they inspired Alan Turing’s 1936 work that launched the theory of modern computation.

After his work in the 1930s, Gödel published only a few papers. His unpublished materials, however, fill tens of thousands of pages and are of great interest to historians of science.

Since 2017, Jan von Plato has led a project at the University of Helsinki to study 16 notebooks Gödel kept in the early 1940s. These so-called working notebooks contain 1,009 pages of dense notes on mathematics and logic. Much of the material is written in Gabelsberger shorthand, a German writing system that was already outdated in Gödel’s lifetime.

Von Plato began the project as he approached mandatory retirement from the university. He decided to tackle Gödel’s mysterious shorthand notes, secured a €2.5 million (£2.1 million) European Research Council grant, taught himself Gabelsberger, and assembled a small team. According to von Plato, only six people in the world can read the shorthand.

Albert Einstein presenting Kurt Gödel (second from right) with an award at Princeton University, where the two became friends. Photograph: Bettmann/Bettmann Archive

Source: theguardian.com

Before Claude joined the effort, the team was working through about one page a week. In August, at a conference in France on AI and theorem proving, von Plato met computer scientists who suggested trying Claude. Back in Helsinki, he gave the model his own transcriptions of the notebooks, along with six of his books about Gödel and other academic literature on the subject.

Within a few days, Claude had produced a 650-page explanation of the notes. Von Plato checked it page by page. He explained that it is difficult for a person to keep the whole collection in mind: researchers usually read one page at a time and forget details, and getting through 50 pages takes about a year. Claude was able to connect information across a thousand pages and treat Gödel’s work as a whole.

Clues to an independent proof

One of Claude’s first tasks was to determine whether the notebooks contained a proof of the independence of the axiom of choice. Such a discovery could support a claim Gödel made in 1966: that he had obtained the result in the 1940s.

American mathematician Paul Cohen received the Fields Medal in 1966, mathematics’ highest honor, for proving the independence of two well-known statements: the continuum hypothesis and the axiom of choice. Gödel said he had already proved the result in the 1940s, but when colleagues asked him to show the proof, he could not reconstruct it from his notes.

Claude found an almost-complete proof in the notebooks. According to von Plato, Gödel made an error in one definition, although he had used the correct version two years earlier. Von Plato believes that if Gödel had continued working for a few more months, he might have arrived at the correct definition. The researcher also noted that the proof links results from set theory into a single sequence.

Von Plato checked the reconstructed proof using Coq, a mathematical proof-checking program. It passed. In the researcher’s view, if Gödel had published work on the axiom of choice, he might have received the 1940 Fields Medal. Von Plato suggested that Gödel may have felt Cohen’s award especially keenly as a missed opportunity.

A microfilm image of an example of Gödel’s shorthand from one of his notebooks. Photograph: Institute for Advanced Study

Source: theguardian.com

What else the notes revealed

Later, von Plato asked Claude to identify every theorem for which Gödel had a complete proof, a sketch, or at least an idea for a proof. The model found 663 results. When checked in Coq, about 400 held in their original form, roughly 200 needed corrections — for example, a more precise statement or an added condition. Around 50 results proved incorrect. Von Plato noted that Gödel himself sometimes reread his notes and wrote “falsch!” (“wrong”) or “schlecht!” (“bad”) in the margins.

The notebooks contained more than a dozen topics in logic and the foundations of mathematics that, according to Claude’s assessment, had not been studied for more than 80 years after Gödel wrote them down. Von Plato plans to continue studying the manuscripts and, after finishing his current projects in logic, turn to Gödel’s notebooks on physics and cosmology.

Historical assessment

Joel David Hamkins, a professor of logic at the University of Notre Dame in Indiana, has not seen Claude’s reconstruction of the proof of the independence of the axiom of choice. He said that if the proof withstands scrutiny, it would be notable and historically important, but researchers still need to determine what Claude contributed and what Gödel contributed.

According to Hamkins, the resemblance between the notes and Cohen’s proof does not by itself mean Gödel already had a finished result: it shows that he was moving in that direction. Hamkins added that work people never shared with anyone is not credited to them, but Gödel’s many groundbreaking ideas make substantial discoveries in his notebooks unsurprising.

Dataist’s take: Claude served as a tool for finding connections in a large archive, while the mathematical value of the results was checked separately, including with Coq. The historical conclusion remains cautious: the notes show how far Gödel had advanced, but they do not settle what exactly he managed to prove and communicate to others.