Comment by well_ackshually
9 hours 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.
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.