6 ms·

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 comm

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.

ksoped 5d ago
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.
- SJMG 5d ago
  Denial of service is the established term. Hammering their API (reviewer committees) would be an informal one
tmhn2 5d ago
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).
charcircuit 5d ago
OpenAI avoids this by formally verifying the proof. https://github.com/openai/NavierStokesAndEuler https://github.com/openai/NavierStokesAndEuler
- well_ackshually 5d ago
  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.
  - charcircuit 5d ago
    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.
    - well_ackshually 4d ago
      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.
      - pyentropy 4d ago
        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?
        well_ackshually 4d ago
        >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.
        pfdietz 4d ago
        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.

ksoped 5d ago

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.

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

tmhn2 5d ago

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).

charcircuit 5d ago

OpenAI avoids this by formally verifying the proof. https://github.com/openai/NavierStokesAndEuler https://github.com/openai/NavierStokesAndEuler

well_ackshually 5d ago
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.
- charcircuit 5d ago
  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.
  - well_ackshually 4d ago
    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.
    - pyentropy 4d ago
      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?
      - well_ackshually 4d ago
        >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.
        pfdietz 4d ago
        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.