Hacker News Reader

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.

View on HN

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?

Reply on news.ycombinator.com