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 2 hours ago | parent [-]

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 an hour ago \| parent [-]
		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.