Hacker News Reader

Comment by ThrowawayR2 | Hacker News Reader

Terence Tao says something surprisingly similar in a recent talk (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.

View on HN

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.

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.

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.

A counterexample (at least the jacobian conjecture one) is a lot easier to manually verify than 10MB Lean proof

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?

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.

He also made a video on the same topic for Big Think: https://news.ycombinator.com/item?id=49551848

Reply on news.ycombinator.com