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

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.