6 ms·

Such a result should be considered worthless: the proof is 10MB of Lean. (https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186). I can

Such a result should be considered worthless: the proof is 10MB of Lean. (https://github.com/openai/PrimeGaps186 https://github.com/openai/PrimeGaps186). I can't think of a single mathematical proof being anywhere close to ten million characters. For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. Humanity gets zero value from that, aside from "some bot seems to think it's 186". Unusable by anyone.

tzs 13d ago
The proof of the classification of finite simple groups is bigger than that.
nicce 13d ago
Yeah. Unless human can verify it, not sure if it is certain or useful.
- kolinko 13d ago
  Wasn’t the proof of Fermatt’s Last Theorem proof similar in complexity?
  - jptlnk 13d ago
    It's probably not 10MB, but famously the groundwork to prove the statement 1+1=2 is nearly 400 pages in to principia mathematica. That's not even proving 1+1=2, it's just the set-theoretic proofs you need to EVENTUALLY get there.
    - anvuong 13d ago
      Saying "proving 1+1=2" is pretty misleading though. The book deals with all the foundational things needed to set up a mathematical universe where 1+1=2 actually has meaning and is consistent. That setup took 400 pages.
  - iamlucaswolf 13d ago
    Yes. But I think that misses the point. In 1799, Paolo Ruffini published a 500 pages long proof showing that there is no closed algebraic solution for the roots of a polynomial of degree five or higher. The proof is extremely verbose and brute-force, essentially enumerating and checking hundreds of cases by hand. It is by today’s standards insignificant. About 25 years later, Evariste Galois proved the same result in about 95% less space by describing the first general theory of groups and fields. It is considered one of the greatest contributions to mathematics of that century, not because of the result, but because its approach opened up a whole new universe of questions, methods and insight. There would be no AES encryption without Galois. To me, Astras proof looks like Ruffinis proof.
    - kolinko 13d ago
      Touché!
ChrisGreenHeur 13d ago
You talk about modern math and worthlessness at the same time? That’s brave.
- well_ackshually 13d ago
  You can have your opinions about modern math, its usefulness in the world as it is, whether or not knowing if hairy balls can divide by three is actually going to be beneficial for anything but just obscure knowledge's sake. You may even say it's useless. Needless to say, a useless result that absolutely no mathematician will ever read, confirm, understand, agree with or even consider to solve their "useless" problems is an impressive waste of resources.
- twothreeone 13d ago
  Worthless is a pretty good description IMO in the context of what Lean is trying to achieve: "enable correct, maintainable, and formally verified code". Tens of millions of lines of LLM vomit may be many things, but it often turns out to not be correct and certainly not maintainable. Formally verified remains as a thin fig leaf covering the uncomfortable truth that formal methods only provide assurances under assumptions (your toolchain, libraries, compiler, OS, and hardware are "correct" and don't expose some exploitable flaw). It doesn't mean that it cannot improve over time, maybe the proof can be "minified" to a state where human reviewers are able to comprehend it; but as it stands there isn't really much insight or confidence to be gained from the artifact itself.
- smokel 13d ago
  There's a branch of mathematics called "pointless topology" [1]. [1] https://en.wikipedia.org/wiki/Pointless_topology https://en.wikipedia.org/wiki/Pointless_topology
kolinko 13d ago
Iirc some mainstream physycists never acknowledged quantum theory because they couldn’t accept that universe was that unintuitive and hard to understand. Ditto ones that opposed Einstein’s general relativity.
- 3asgfaf 13d ago
  [flagged]
ricardobeat 13d ago
The human-written https://github.com/AxiomMath/PrimeGapsLib https://github.com/AxiomMath/PrimeGapsLib adds up to 4MB of Lean so it's that far off.
- rfw300 13d ago
  Is this human-written? Axiom Math is a company building AI theorem provers, one would think this would also be heavily AI-generated.
ThrowawayR2 13d ago
Terence Tao says something surprisingly similar in a recent talk (https://news.ycombinator.com/item?id=49056620 https://news.ycombinator.com/item?id=49056620 ) Not that the proof is worthless but that the value comes after it's revised into a cleanly understandable form and then canonicalized so that other mathematicians can use it.
- dr_scully 13d ago
  He also made a video on the same topic for Big Think: https://news.ycombinator.com/item?id=49551848 https://news.ycombinator.com/item?id=49551848
- asib 13d ago
  Tao is saying that there is very little insight from something like an LLM counterexample (e.g. Jacobian conjecture counterexample he investigated further on his blog) - you don't learn much about the subject and _why_ a conjecture was true or false from an LLM giving a counterexample. That's why he wrote the blog post - to analyse what the counterexample says about the subject. Tao does not disbelieve the counterexample (it's seemingly easy enough for him to verify it is a counterexample). Parent is saying something very different - they're saying they literally don't have any faith that this is a proof. Given its size, it could just be a bunch of completely useless statements that do pass the type checker.
  - well_ackshually 13d ago
    You're putting a lot of words in my mouth. What I'm saying is that whether or not it's a proof, it's useless: it does not improve human knowledge, because the only thing able to consume 10MB of Lean to build upon it is another LLM that's going to build a 50MB piece of shit. It's very much likely a proof. It's also completely useless.
    - asib 13d ago
      You said: > For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. So you were implying the possibility of there not actually being a proof at all. Anyway, I disagree. I'd refer you to Tao's blog post about the Jacobian conjecture counterexample. The existence of a proof is something you can use, with an LLM, to derive insight, just as Tao did with the existence of the counterexample.
pbkompasz 13d ago
It's like hitting a local minima, it was given a technique, it brute forced it for a lot of money and slightly improved the result. But nothing new was discovered, no new mathematical tool was built, only a huge file that no one will read or build on.

tzs 13d ago

The proof of the classification of finite simple groups is bigger than that.

nicce 13d ago

Yeah. Unless human can verify it, not sure if it is certain or useful.

kolinko 13d ago
Wasn’t the proof of Fermatt’s Last Theorem proof similar in complexity?
- jptlnk 13d ago
  It's probably not 10MB, but famously the groundwork to prove the statement 1+1=2 is nearly 400 pages in to principia mathematica. That's not even proving 1+1=2, it's just the set-theoretic proofs you need to EVENTUALLY get there.
  - anvuong 13d ago
    Saying "proving 1+1=2" is pretty misleading though. The book deals with all the foundational things needed to set up a mathematical universe where 1+1=2 actually has meaning and is consistent. That setup took 400 pages.
- iamlucaswolf 13d ago
  Yes. But I think that misses the point. In 1799, Paolo Ruffini published a 500 pages long proof showing that there is no closed algebraic solution for the roots of a polynomial of degree five or higher. The proof is extremely verbose and brute-force, essentially enumerating and checking hundreds of cases by hand. It is by today’s standards insignificant. About 25 years later, Evariste Galois proved the same result in about 95% less space by describing the first general theory of groups and fields. It is considered one of the greatest contributions to mathematics of that century, not because of the result, but because its approach opened up a whole new universe of questions, methods and insight. There would be no AES encryption without Galois. To me, Astras proof looks like Ruffinis proof.
  - kolinko 13d ago
    Touché!

ChrisGreenHeur 13d ago

You talk about modern math and worthlessness at the same time? That’s brave.

well_ackshually 13d ago
You can have your opinions about modern math, its usefulness in the world as it is, whether or not knowing if hairy balls can divide by three is actually going to be beneficial for anything but just obscure knowledge's sake. You may even say it's useless. Needless to say, a useless result that absolutely no mathematician will ever read, confirm, understand, agree with or even consider to solve their "useless" problems is an impressive waste of resources.
twothreeone 13d ago
Worthless is a pretty good description IMO in the context of what Lean is trying to achieve: "enable correct, maintainable, and formally verified code". Tens of millions of lines of LLM vomit may be many things, but it often turns out to not be correct and certainly not maintainable. Formally verified remains as a thin fig leaf covering the uncomfortable truth that formal methods only provide assurances under assumptions (your toolchain, libraries, compiler, OS, and hardware are "correct" and don't expose some exploitable flaw). It doesn't mean that it cannot improve over time, maybe the proof can be "minified" to a state where human reviewers are able to comprehend it; but as it stands there isn't really much insight or confidence to be gained from the artifact itself.
smokel 13d ago
There's a branch of mathematics called "pointless topology" [1]. [1] https://en.wikipedia.org/wiki/Pointless_topology https://en.wikipedia.org/wiki/Pointless_topology

kolinko 13d ago

Iirc some mainstream physycists never acknowledged quantum theory because they couldn’t accept that universe was that unintuitive and hard to understand. Ditto ones that opposed Einstein’s general relativity.

3asgfaf 13d ago
[flagged]

ricardobeat 13d ago

The human-written https://github.com/AxiomMath/PrimeGapsLib https://github.com/AxiomMath/PrimeGapsLib adds up to 4MB of Lean so it's that far off.

rfw300 13d ago
Is this human-written? Axiom Math is a company building AI theorem provers, one would think this would also be heavily AI-generated.

ThrowawayR2 13d ago

Terence Tao says something surprisingly similar in a recent talk (https://news.ycombinator.com/item?id=49056620 https://news.ycombinator.com/item?id=49056620 ) Not that the proof is worthless but that the value comes after it's revised into a cleanly understandable form and then canonicalized so that other mathematicians can use it.

dr_scully 13d ago
He also made a video on the same topic for Big Think: https://news.ycombinator.com/item?id=49551848 https://news.ycombinator.com/item?id=49551848
asib 13d ago
Tao is saying that there is very little insight from something like an LLM counterexample (e.g. Jacobian conjecture counterexample he investigated further on his blog) - you don't learn much about the subject and _why_ a conjecture was true or false from an LLM giving a counterexample. That's why he wrote the blog post - to analyse what the counterexample says about the subject. Tao does not disbelieve the counterexample (it's seemingly easy enough for him to verify it is a counterexample). Parent is saying something very different - they're saying they literally don't have any faith that this is a proof. Given its size, it could just be a bunch of completely useless statements that do pass the type checker.
- well_ackshually 13d ago
  You're putting a lot of words in my mouth. What I'm saying is that whether or not it's a proof, it's useless: it does not improve human knowledge, because the only thing able to consume 10MB of Lean to build upon it is another LLM that's going to build a 50MB piece of shit. It's very much likely a proof. It's also completely useless.
  - asib 13d ago
    You said: > For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. So you were implying the possibility of there not actually being a proof at all. Anyway, I disagree. I'd refer you to Tao's blog post about the Jacobian conjecture counterexample. The existence of a proof is something you can use, with an LLM, to derive insight, just as Tao did with the existence of the counterexample.

pbkompasz 13d ago

It's like hitting a local minima, it was given a technique, it brute forced it for a lot of money and slightly improved the result. But nothing new was discovered, no new mathematical tool was built, only a huge file that no one will read or build on.