5 ms·

Terence Tao says something surprisingly similar in a recent talk (https://news.ycombinator.com/item?id=49056620 https://news.ycombinator.com/item?id=49056620 )

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.
    - pcloadlett3r 11d ago
      A counterexample (at least the jacobian conjecture one) is a lot easier to manually verify than 10MB Lean proof
  - cman1444 12d ago
    If we accept that it is a proof then it does improve human knowledge, even if no one can understand how to get there. If you were navigating a pitch dark cave, wouldn't you find it useful to be able to see the light of the cave opening even if it's not bright enough to illuminate your path to it?
vessenes 13d ago
I'd like to note that we should remember a formalized Lean proof does have value in that it enters the pantheon of true things other Lean proofs can rely on. Agreed that for the humans, descriptions and being able to 'grok' the proof / assess it for new tools and concepts is extremely helpful.

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.
  - pcloadlett3r 11d ago
    A counterexample (at least the jacobian conjecture one) is a lot easier to manually verify than 10MB Lean proof
- cman1444 12d ago
  If we accept that it is a proof then it does improve human knowledge, even if no one can understand how to get there. If you were navigating a pitch dark cave, wouldn't you find it useful to be able to see the light of the cave opening even if it's not bright enough to illuminate your path to it?

vessenes 13d ago

I'd like to note that we should remember a formalized Lean proof does have value in that it enters the pantheon of true things other Lean proofs can rely on. Agreed that for the humans, descriptions and being able to 'grok' the proof / assess it for new tools and concepts is extremely helpful.