Hacker News Reader

Comment by well_ackshually | Hacker News Reader

So it wasted everyone's time, thousands of hours of research trying to disprove something said very loudly. What OpenAI is doing is a DoS of the scientific community: wasting your time trying to check if they're not wrong, and claiming glory in the mean time.

View on HN

That's true, but the story would have unfolded differently if Mochizuki had a lean-verified proof and was correct. I guess baked into my premise is that AI is producing reliable proofs (in the long term at least).

OpenAI avoids this by formally verifying the proof.

https://github.com/openai/NavierStokesAndEuler

It doesn't. It's 32 millions lines of bullshit, and the only thing it brought is "it's not true in some extreme conditions lol". The effort needed to figure out why that is, what conditions lead to it, the new mathematics that would need to be developed to solve their problem is once again being hoisted on actual humans, who now need to waste their time sifting through their slop.

You don't have to read 32 million lines. You can just look at what got proved. The proof checker lets you trust those millions of lines you did not read.

No, you don't understand: that proof is useless. When you solve mathematical problems, you open up new ones in the process of doing so. You create new research. You create new theories, new notations, new thought.

This is just ticking a checkbox. And even worse and more time wasting even: you have ZERO proof that there's no latent Lean bug. Especially in a proof this large.

Not a Lean expert but some of the proof tactics used to prove are probably novel? Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?

>Not a Lean expert but some of the proof tactics used to prove are probably novel

Maybe. But they're in 32 millions lines of Lean. How do you find the needle in the haystack ?

>Or, you could prompt agents later to analyze which lemmas or parts of the proof are surprising or applicable to other problems?

If OpenAI was truly serious about improving maths (and not jerking themselves off), they'd have also used Prove2Me (and contributed their results back), which would have done that. Each part of the proof combines into a larger graph, that everyone can reuse. Note that Anthropic isn't better there: yes, they used Prove2Me, but as far as I know they haven't contributed back to it, and just shat out 10 million lines and a good luck everyone.

Leaf dumps out a proof object that can be verified to be correct. Absent a bug in the verifier, you can trust it, probably more than you can trust a human-produced proof. This is why Lean was a thing even before AI.

s/Leaf/Lean/

LLMs are good at finding the needle in the haystack. All efforts now should be in figuring out how to make LLMs get as good as possible at math.

Agreed! Although, if done by a mathematician, it's not a ~complete waste. I think the community learns something along the way.

Is there an established term for the idea of "DoS"? I've taken to calling it slop fatigue.

Denial of service is the established term. Hammering their API (reviewer committees) would be an informal one

Reply on news.ycombinator.com