Formalizing Fermat's Last Theorem
6 points by ni5arga
6 points by ni5arga
Rumor has it that one of the labs already solved a Millennium Prize problem. True or not, at this point it would not surprise me at all any more.
Unless it’s very recent, why would any lab sit on that finding? I feel like the risk of the other lab racing to a similar announcement is too high.
It makes sense to wait to announce it to match commercial reasons - for example, to generate good PR for an investment round or IPO.
It’s probably both recent and because the way these proofs work is that they at massive LEAN programs with millions of lines of code. They both need to validate that they did not run into LEAN bugs and a human needs to validate it.
This is Dexter's Laboratory thinking. Maybe, at best, it's Hangar 18 thinking. Not only have you brought no evidence to the table, thus resulting in a trivially discardable claim, but the claim begs for its own belief; instead of evidence, you're portraying Chris Farley's bus driver who insists that it would be very cool if the claims were true.
Rumor is that the big labs are all incompetent; they are years behind in R&D, selling products that harm people, and trying to fundraise instead of providing high-quality services. This sort of spectacle, where the big lab takes an already-known human achievement and tries to imitate it poorly with sheer CPU time, is meant to raise funds for the lab rather than to give back to any community. In this case, Anthropic has given the mathematical community a totally-unusable from-scratch hair-shirt and is hoping that somebody will perform the masochistic ritual of wearing it in public.
The resulting proof can be found in this repo: https://github.com/anthropics/fermats-last-theorem