Top
Best
New

Posted by bookofjoe 6 hours ago

AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems(www.theguardian.com)
303 points | 88 commentspage 2
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
zapataband2 3 hours ago|||
[dead]
rsoto2 1 hour ago|||
decades of OCR research is not trivial. What's stupid is being gullible
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|||
If he was facing mandatory retirement nearly ten years ago it’s likely he might be ready for voluntary retirement, particularly after achieving this fantastic result.
bananaflag 3 hours ago||
Indeed, he is 75 years old.
vorticalbox 3 hours ago|||
I would his not be in verifying the AI is output?
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|||
He might see his value in his role of carrying the knowledge itself rather than being its gatekeeper.
cloudbonsai 1 hour ago||||
I actually got a very different impression. He could publish this interesting result, exactly because he had been working on this project i.e., had an interesting dataset to feed into Claude and had the expertise to interpret its output.

Compare him to those who are burning tokens to generate cringeworthy AI slop on social media. The value of a tool depends on the skill of the user.

mohamedkoubaa 3 hours ago|||
And he didn't want to milk that for the rest of his life because he's a smart guy that has other skills and interests
ShinyLeftPad 5 hours ago|||
That's what he thinks, surely.
bdamm 5 hours ago|||
It's clear though. Even if an AI had connected all the dots on the obsolete shorthand, it would never have recognized the human value. I doubt that any AI process would choose to spend the energy on interpreting this particular obsolete handwriting and then understand that it was from the hand of a genius.
ShinyLeftPad 5 hours ago||
But is he needed once he finished writing the prompt?
jvanderbot 5 hours ago|||
Using AI to do your job does not mean that AI suddenly walks in the door and escorts you out and starts collecting your paycheck.

Someone is still driving these studies, and probably will be for a while. Or maybe not. But still we can reward this guy for opening up this can of theorems that had before.

Silliest case: Imagine a dusty basement terminal screen open to claude code with "There we go! Cancer is cured as you requested, let me know and I'll send off the results" and nobody is around to approve it.

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
y6543987 23 minutes ago||
typical newspaper blown up wording.
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...

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||
There was also a project to catalog and prove all the theorems in Ramanujan's notebooks. There's a book series by Bruce C. Berndt which covers the 5 notebooks:

https://www.amazon.com/stores/Bruce-C.-Berndt/author/B001HN3...

It would be interesting to point Fable or Argon at the notebooks and see if they can find some interesting new material in or based on this work.

Aboutplants 4 hours ago||
The line between Genius and Crazy is but hairs width
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||
Yes, you can. So maybe we'll see an adoption of that paradigm, or another. The value of a ZKP is that you can optionally prove some facts up front about the file, whereas a normal hash is all-or-nothing. You can't reveal part of the information because you need the entire contents to properly verify the hash.
mjd 2 hours ago|||
ceiiinosssttuv
soulofmischief 2 hours ago||
Thanks for putting me onto this, that was new to me. And of course Huygens was all over this idea.
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||
True.
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".
More comments...