Hacker News Reader

Comment by bananaflag | Hacker News Reader

I find it weird to blame OpenAI for using math as a benchmark. If they hadn't done so, then in three months, say, after releasing Bel, someone else would have used math as a benchmark for it (like mathematicians already do since Fable 5 and 5.6 Sol). The result would have been the same (hundreds of open problems solved quickly).

View on HN

We had to build the Torment Nexus, because otherwise, someone else would have built the Torment Nexus.

No, that's not what I say. My argument is that once the Torment Nexus is built, it is stupid to argue that they used it to torment people, when someone else would have tormented people with it anyway. If one wants to argue something, it's that the Nexus should not have been built.

And I honestly have no idea what Tao wanted to happen. How could you ensure that the AI "empowers" scientists and doesn't replace them. Intelligence is intelligence. If it's powerful enough, it will replace other intelligence.

> No, that's not what I say

Unfortunately, though, it is what you said. And more or less what you

> If one wants to argue something, it's that the Nexus should not have been built.

Or that it is being built in a way that is causing forseeable problems, while making no effort to anticipate and solve or mitigate those problems.

It’s more like: we had to build the Torment Nexus, because otherwise, people used its non-existence as evidence we couldn’t.

> The result would have been the same

No? How much did OpenAI spend on this and how many trials failed? I can’t imagine anyone not working for them can pay the absurd token costs!

But distributed over thousands of people, I see it happening. Maybe a bit slower, but still.

> distributed over thousands of people

Can you elaborate what does that look like?

A few people spend all their focus and tokens on one problem, and after some time I expect one of them to get at least closer to a solution. They can either work independently, or even better they team up and create a shared scratchpad for their agents. I don't see limits to scaling this, compared to OpenAI running however many subagents per problem.

And that multiply those few people by number of different problems.

I very much wish they'd just let mathematicians have at it empowered by the model so we could all treat the people who claim they have a lean verified proof with an unintelligible explanation as the crackpots they are.

I know this can feel like little consolation, but mathematicians were lucky that OpenAI simply dumped their early results in a messy GitHub repository, rather than publishing hundreds of polished articles three months from now.

It isn’t a benchmark though. Not yet. They rely on mathematicians to check the proofs including all lemmas. And on other mathematicians checking the reviews. Without being on the OpenAI payroll of course. Now they have flooded the zone, overwhelming the review capacity of the whole field by at least one order of magnitude. It is the move of 15-year-olds holding tools they shouldn’t have access to.

LEAN.

Did they force anyone to focus on reviewing those results instead of other ones? People choose to focus on them for a reason.

I think it's always better to publish preliminary results early (as long as you clearly say so, and they did), and let mathematicians decide which of those are worth focusing on.

They did not do this in a vacuum. But it doesn’t matter much. Benchmarking needs a benchmark.

Reply on news.ycombinator.com