Though that's not her latest paper.
"No independent human semantic review. Whole-file sorry counts and a complete auxiliary-declaration audit are not established; separate declaration lint has not been run."
The reason I think this is interesting is that Axiom is a tiny lab in comparison that wouldn't have had access to Astra at all. I'd be curious to learn how Axiom is able to effectively compete at this frontier with vastly fewer resources.
edit: my comment was on the submission for https://github.com/openai/PrimeGaps186 but seems to have been moved to the main Astra submission
Why would you think it was an employee who did the push, instead of a random GPT agent?
I can't think of a single mathematical proof being anywhere close to ten million characters. For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. Humanity gets zero value from that, aside from "some bot seems to think it's 186". Unusable by anyone.
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.