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.
It's very much likely a proof. It's also completely useless.
> 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.
Ditto ones that opposed Einstein’s general relativity.
In 1799, Paolo Ruffini published a 500 pages long proof showing that there is no closed algebraic solution for the roots of a polynomial of degree five or higher. The proof is extremely verbose and brute-force, essentially enumerating and checking hundreds of cases by hand. It is by today’s standards insignificant.
About 25 years later, Evariste Galois proved the same result in about 95% less space by describing the first general theory of groups and fields. It is considered one of the greatest contributions to mathematics of that century, not because of the result, but because its approach opened up a whole new universe of questions, methods and insight. There would be no AES encryption without Galois.
To me, Astras proof looks like Ruffinis proof.
It doesn't mean that it cannot improve over time, maybe the proof can be "minified" to a state where human reviewers are able to comprehend it; but as it stands there isn't really much insight or confidence to be gained from the artifact itself.
Needless to say, a useless result that absolutely no mathematician will ever read, confirm, understand, agree with or even consider to solve their "useless" problems is an impressive waste of resources.