Comment by piloto_ciego
11 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.
11 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
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?
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"
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.
I. fucking. Wonder. Why.
https://news.ycombinator.com/item?id=49607239