Comment by piloto_ciego
16 hours ago
How can you possible say this sort of thing in context of what looks like a millenium prize being solved.
I swear there's nobody blinder than those who won't see.
16 hours ago
How can you possible say this sort of thing in context of what looks like a millenium prize being solved.
I swear there's nobody blinder than those who won't see.
Because it seems like most of the work may have been done by human mathematicians and cribbed by OpenAI at the last minute
The human mathematicians didn't solve the Navier-Stokes problem, they solved the Euler problem. And they were extensively using LLMs to drive the work, as described in the Buckmaster statement.
Any way you cut it, this is a major achievement for AI, besotted with human drama over whose prompt should be recognized by the history books.
We don't have enough accurate knowledge to say that, and it doesn't seem to be the case at all.
> We don't have enough accurate knowledge to say that, and it doesn't seem to be the case at all.
The first part of your sentence literally contradicts the second part: "we don't have enough knowledge to know, but I know the opposite".
6 replies →
> it doesn't seem to be the case
Based on what? Your crystal ball?
1 reply →
I don't think we should assume a millenium puzzle has been solved, yet. Astra showed impressive capacity for cheating when it was faced with impossible cybersecurity challenges. It seems equally plausible at this stage that it's found a bug in Lean.
You have to look at the incentives
I swear to god, people would look at the successes of Xerox palo alto and just shrug and say - "yeah, but I mean, this is all marketing"
Xerox is incidentally a really good example, because precisely nobody ended up using the desktop experience Xerox made. They ended up using the desktop experience that Microsoft and Apple made and shipped while Xerox the actual company faded and memory of those original parc research teams faded into obscurity.
This is what I keep saying, and it feels like I'm taking crazy pills here!
Is nobody else astounded by this?
Incentives are one thing, even adjusting for them it's huge, and I don't understand this incentive play for only openai, academics have perverse incentives too, to overreport, overclaim, publication bias etc why are we scrutinizing AI industry to such high degree when they have demonstrated capability and often times are off by a model release at worst.
A working Lean proof doesn't care what the incentives are.
How? By being knowledgeable, intelligent, and intellectually honest.
People will cling to views as long as they possibly can, despite evidence slapping them in the face.
Eventually it won't matter. Arguments over whether LLMs are "truly" intelligent are going to be a matter of philosophy, and look a little silly.
I. fucking. Wonder. Why.
https://news.ycombinator.com/item?id=49607239