AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems (theguardian.com)

298 points by bookofjoe 6 hours ago

hobo123 5 hours ago

The stuff about Gabelsberger shorthand sounds ludicrous to me. My father would write notes in a custom version of it until his death 2020.

Officially (i.e. in schools teaching stenography, back in the day) it was long ago replaced by "unified German shorthand" (Deutsche Einheitskurzschrift IIRC), but he always considered Gabelsberger to be superior.

Well, maybe he too was one of the 6 people in the world who could read it (or yes, maybe that was hyperbole, I'm not sure) :D

semolinapudding 4 hours ago

I think it's 6 people who can read Gabelsberger and know enough mathematical logic to make out what Gödel is saying.

throwaway81523 an hour ago

The notebooks were transcribed to regular German by a couple[0] who learned Gabelsberger just for that purpose. There is a bunch of analysis of them in Gödel's 5-volume Collected Works, iirc mostly volume 4. I'm surprised if there was any interesting mathematical content left to be found. The question that mathematicians wondered about the most was whether Gödel made any progress on the independence of the continuum hypothesis and axiom of choice (both later proved by Cohen). It appeared that he had some thoughts about it but didn't get anywhere. The Guardian article says Gödel was close to a proof of AC's independence but I'm skeptical.

The question the public wondered about the most was the loophole Gödel claimed to have found in the US Constitution, but they didn't find anything about that.[1]

There's a cool suspense novel "The God Proof" about finding a lost Gödel notebook extending Gödel's ontological "proof" of the existence of God.[2]

0. John Dawson (a logician) and his wife whose name I think is Cheryl (not sure). John Dawson later wrote the Gödel biography "Logical Dilemmas".

1. https://en.wikipedia.org/wiki/G%C3%B6del%27s_loophole

2. https://jeffreykegler.github.io/personal/gp/God_Proof.pdf

aaronrobinson 2 hours ago

I read it as knowing it at all but maybe it’s the mathematical shorthand subset.

iltennico 4 hours ago

From what historians of science tell us, Gödel was in any case an absolute perfectionist who mostly published work that was bulletproof. His enormous body of notes surely contained some very sharp insights, but it is unlikely that he would have produced illuminating, conclusive new theorems by chance and without realizing it. He was a very harsh reviewer of his own work.

bananaflag 3 hours ago

He did discover the functional interpretation in 1940 and publish it only in 1958, so it is highly probable that he has valuable unpublished results.

blurbleblurble 4 hours ago

Maybe it's likely that he didn't have proofs, but surely had all kinds of theorems with at the very least some intuition of a proof. Recall that he wouldn't have had the same huge breadth and depth of mathematical machinery available to him that we have now.

breezybottom 3 hours ago

You could just read the article instead of speculating about what's in it. This isn't reddit.

agosz 2 hours ago

Yes, it does state they found proofs and new theorems but also false ones too. I'm curious what new insights the ones that were proved hold.

It's really cool how AI is just able to decipher these and validate them with automated theorem provers. Crazy times!

imbiased 5 hours ago

I can't remember the exact quote but I believe I read that Gödel confided to Einstein (in their walks in Princeton) on his deep worry of his work being forgotten. If only he knew.

shepherdjerred 3 minutes ago

Anxiety is a great motivator

writtenone 3 hours ago

Now in 2026 every store use facial recognition to make sure you are ALWAYS remembered.

kridsdale1 3 hours ago

For short geological time horizons at least.

agnosticmantis 3 hours ago

AI did not comment on the consistency or completeness of the notebooks.

bad_username an hour ago

True! but unprovable.

pryelluw 3 hours ago

Funny thing is your comment is consistent and complete.

acjohnson55 2 hours ago

This is possible for things that have less power than arithmetic!

ducttapecrown 6 hours ago

It'd be interesting to hear about these new 14 themes of logic Gödel pursued!

calf 4 hours ago

Article also mentions his notes were a few months work away from proving independence of CH decades before Cohen's result in 1963.

bahbahbahbah 5 hours ago

Yeah, these notes need to be just openly published. Then I could ask my own Claude for an explanation. (Not /s)

aaronrobinson 2 hours ago

Or just share the Claude sessions as Tao did his.

rsoto2 4 hours ago

You could likely "unlock" the manuscript yourself with a competent computer vision algorithm. It's nothing that fancy.

Perseids 4 hours ago

sally_glance 3 hours ago

That would be the future of crowdsourcing - by submitting the same prompt as 1000 other people, you're basically donating your tokens to the cause of maybe spotting a valuable insight the others didn't get because of random output sampling :)

evolve2k 2 hours ago

Very much need a statement in there as to if AI was used in the making of the manifesto, goes to the heart of the ethical soul of the manifesto.

I’d suggest you bake it into that header line on writtten by; something like this (but edited depending how ai was used):

“Written without AI assistance by the speakers and attendees of AIE Code Summit 2026 ”

cobychapple 2 hours ago

Was this comment meant to be on the other neighbouring link (No AI Slop: A Manifesto - https://news.ycombinator.com/item?id=50488769)?

semolinapudding 6 hours ago

This is incredibly exciting! Gödel is unquestionably the most important logician in history, but unfortunately he published very little. For instance, the Dialectica interpretation was published approximately 20 years after his first ideas on the subject.

Plus, Jan von Plato is the world's leading expert on Gödel -- the number of people who can read Gödel's handwriting can be counted on the fingers of one hand, and I think that every single one is part of Jan von Plato's research group. If he is excited about the output, this is a huge deal.

tetris11 2 hours ago

Let's try the Voynich Manuscript next

empath75 6 hours ago

https://aitp-conference.org/2026/slides/JvP.pdf this seems to be slide deck with some of the results.

superjan 5 hours ago

And here is the site of the research group involved. https://www.helsinki.fi/en/researchgroups/godel-enigma

taylorbuley 5 hours ago

Thank you! Godel's work get us comfortably uncomfortable with unknowability but damn, to think there's more out there! I'm dying to know more.

tiffanyh 4 hours ago

I’m been trying to use various frontier models to decipher lost ancient languages (like Linear A).

I wonder what tactics this used, so that I can leverage in my own work.

rhdunn 3 hours ago

The problem with Linear A is that we don't have a reference point like the Rosetta Stone to anchor it to other languages and scripts. It also has a small corpus, making it hard to find patterns in the texts.

jdelman 4 hours ago

I wonder how much expertise was actually needed to translate these notebooks. In other words, could a general purpose model one-shot these translations, or did we really need a subject matter expert to do the work? BTW - I'm not saying having a subject matter expert tackle the problem with Claude isn't useful - just wondering what the limits are!

rsoto2 4 hours ago

Uh, a decades old properly trained OCR algorithm could probably "unlock" these manuscripts

semitones 3 hours ago

Right you are - this was "trivial", and everyone is "stupid" - except for you

rsoto2 an hour ago

sheikhnbake 5 hours ago

This might be an actual concrete example of someone making themselves obsolete with AI.

> Von Plato said he had started his Gödel project in 2017 because he was facing mandatory retirement from Helsinki University. “What should I do to make myself indispensable? Oh yes, I’ll start reading Gödel’s enigmatic shorthand pages!” He received a €2.5m (£2.1m) grant from the European Research Council, taught himself Gabelsberger shorthand – “I am one of only six people who can read it in the world” – and assembled a small team.

snk 5 hours ago

And via earthshaking victory, at that, wow.

arbot360 4 hours ago

Okay let me know when AI gets itself a 2.1M Euro grant from ERC as the PI.

sheikhnbake 4 hours ago

I think you're missing my point. It's that once the workbooks are completely interpreted, which is happening at an accelerated pace thanks to AI, von Plato's value as an interpreter of the short hand becomes severely reduced, presumably as does his ability to get future grants.

I'd think there would be more competition to lead studies and receive grants now that the workbooks are accessible to a wider audience of logicians

enneff 4 hours ago

vorticalbox 3 hours ago

alterom 5 hours ago

It's literally an example of someone keeping themselves from becoming obsolete with AI.

sheikhnbake 5 hours ago

The professor's value was/is in being one of a few people with the capability of interpreting the shorthand. By translating it with AI, his value as an interpreter begins evaporating as the translated workbooks become accessible to more logicians.

Bayart 4 hours ago

cloudbonsai 35 minutes ago

mohamedkoubaa 3 hours ago

ShinyLeftPad 5 hours ago

That's what he thinks, surely.

bdamm 5 hours ago

jvanderbot 5 hours ago

rjsw 4 hours ago

Maybe the notebooks will contain details of his "loophole", or maybe it will have been proven true in real life by then.

GodelNumbering 3 hours ago

> Gödel himself, when rereading his notes, would occasionally add a marginal remark: falsch! [incorrect] or schlecht! [bad].”

This is probably my favourite part of the article. On brand.

Muhammad523 2 hours ago

I first came to know about Gödel's incompleteness theorem while watching a video by Veritasium (https://www.youtube.com/watch?v=HeQX2HjkcNo), it's around 30 minutes but a really good video. It's from the time before Veritasium became slop. The video talks about many things that are interconnected, like the halting problem, undecidable systems like the game of life, Hilbert's dream of a finite set of axioms to prove all mathematics, and, of course, a perfect explanation of Gödel's incompleteness theorems

insane_dreamer 5 hours ago

> Increasingly paranoid in his later years, he refused to eat food that was not cooked by his wife, and died of starvation in 1978

genius often comes with side effects

e28eta 4 hours ago

This extra detail makes the story even sadder, imo:

> Following Adele's admission to hospital after suffering a stroke in late 1977, Gödel refused to eat in her absence; he weighed 29 kilograms (65 lb) when he died of "malnutrition and inanition caused by personality disturbance" in Princeton Hospital on January 14, 1978

https://en.wikipedia.org/wiki/Kurt_Gödel#Personal_life_and_d...

Aboutplants 4 hours ago

The line between Genius and Crazy is but hairs width

Bayart 4 hours ago

My favourite end-of-life weirdo has to be Grothendieck.

QuesnayJr 4 hours ago

There is a similar project to digitize and analyze Grothendieck's notes and letters.

programd 2 hours ago

alterom 5 hours ago

"You don't get credit for the work you don't tell anybody about"

This has been a problem long before Godel: famously, Newton tried to get credit for inventing Calculus only after Leibniz published his work, leading to a bitter dispute that lasted long after they both died.

I wonder if this problem is now going to be significantly exacerbated by AI, as mathematicians are getting more incentives to keep their works secret —

— or, to the contrary, the community will get a push to publish incomplete ideas, scratch work, etc. early to establish a record of thinking about a problem before others did.

In the end, as always, it's a social problem created by " publish or perish " institutional incentives which reward (and require!) published results, but not the work that led to to them.

This, I hope, will finally change.

soulofmischief 5 hours ago

Maybe we'll see a solid societal use case for zero-knowledge proofs here, establishing one had a set of documents at a given date without revealing them.

_bent 5 hours ago

you can just write a doc with your proof/idea, hash it and post that hash on twitter

soulofmischief 2 hours ago

mjd 2 hours ago

ceiiinosssttuv

soulofmischief 2 hours ago

ShinyLeftPad 5 hours ago

so what would the new incentives be? don't publish... and get paid anyway?

hobo123 5 hours ago

At least that's how traditional Western universities used to work. The profs sometimes published something, and they taught students. Looking at science back then, it seemed to work out rather well.

ShinyLeftPad 5 hours ago

mohamedkoubaa 3 hours ago

If possible, this would be ideal.

kyle-rb 3 hours ago

A little disappointed to learn it was a guy prompting and not an OpenAI agent swarm reward hacking the goal of "prove as many theorems as possible".

grokgrok 3 hours ago

I hear they're all incomplete

2aFds 6 hours ago

Nice timing for the IPO. Cooked Nvidia numbers on the 17th are still missing, and the 19th will go well!

The AI was of course trained on existing pre-AI transcriptions of Goedel's shorthand, which he was taught in school around 1920 and which was widespread and only technically "obsolete".

https://link.springer.com/book/10.1007/978-3-030-67606-3

letmevoteplease 5 hours ago

In the first paragraph, we have an evidence-free insinuation that the foremost expert on this subject is some kind of shill running a campaign for Anthropic. What does this campaign involve? Is he just making it all up? Let me hear your theory of what is happening here and how it invalidates the claimed abilities of the model (or why the abilities do not matter).

In the second paragraph, we have what appears to be a claim that the model knows how to read Gödel's shorthand because it has been exposed to past examples of that shorthand. What is your point here? I think the model learning to generalize by training on a few examples is a point in its favor.

cyanydeez 6 hours ago

I think we'll find godel's most pungent critiques of modern logic & mathmatics to be the maddening limits of LLMs.

LdBaringSwallow 5 hours ago

Why? His incompleteness work explains why software and math suck so he would already expect them to; they're rhetorical and can never fully be a closed loop body of knowledge as we can never with rhetoric concretely observe/define the far future or far past; merely simulate rhetorically

Ergo all defined axiomatic systems have sentences about the far past and future that cannot be defined in those languages with certainty. Most do not make the connection to physics. Gödel did and would 100% aware the limits exist and will always exist

Scaling laws aren't just for computers; humans cultures do not scale infinitely through time, just approximately 2-3 generations

As I understand immutable physical truth like this played a huge role in his early research and ultimately were the forcing function that led him to incompleteness

kevin42 4 hours ago

"all defined axiomatic systems have sentences about the far past and future that cannot be defined in those languages with certainty."

This is often misunderstood or misstated to mean that there are some things that are unknowable or unable to be solved. (I'm not saying that's what you were implying, I am referring to the common way I see his theorem being represented)

But what he really proved is that no single sufficiently powerful, consistent, effectively specified formal system can prove every arithmetic truth.

He didn't prove that there are mathematical truths that are unsolvable through any possible extension or alternative framework. It's just that one framework isn't enough to solve all problems.

LdBaringSwallow 2 hours ago

rsoto2 4 hours ago

"Unlocks" cool so Claude the trillion dollar technology did what any funded researcher with a computer vision algorithm could have done years ago. Wow so impressive.

CrimsonRain 2 hours ago

Why didn't they do it then?

michaelhoney 4 hours ago

This kind of comment is ignorant and damaging to HN.

Do better.

rsoto2 an hour ago

AI sycophancy is ignorant and damaging to HN. So is misattributing decades of OCR research to the company that stole everyone's data.