141–150 of 525 posts
I can recommend the book telling the full story behind Fermats Last Theorem (by Simon Singh). It’s quite fascinating, and paved with really, _really_ weird characters each chipping in on the final solution.
- https://www.youtube.com/watch?v=nUN4NDVIfVI (The bridges to Fermat's Last Theorem)
- https://www.youtube.com/watch?v=NPOw4iIxN6o (podcast)
Holy shit, this has to be one of the most difficult proofs to formalize due to it's length and complexity right?
Yep. There may be only 25-50 people alive today in the whole world who can credibly claim to understand Wiles' proof. Now we add an LLM to that list. Absolutely mind-blowing stuff.
No we cannot. LLMs do not, by their very nature, understand a single thing. You are giving far too much credence to hype and marketing.
Earlier quoted context omitted.
Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
I don't think Anthropic is turning a profit ;)
Impressive! Buzzard's group[1] got scooped. [1] https://github.com/ImperialCollegeLondon/FLT
> I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project, and indeed it goes much further in terms of what is formalized (I only promised the EPSRC that I would reduce FLT to the 1980s; this repo proves the whole thing). But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. My guess is that it is unlikely that Anthropic are going to do this; they will feel that their job is done with the formalization (and they did not formalize the modern proof anyway).
> Note that mathematically this work of anthropic tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK, and most people in the number theory community are 100% sure (formalization has made me more paranoid about the mathematical literature than most). From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.
https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...
but i don't understand... isn't Wiles's proof and its numerous rewritings already in the training set?
To ask a dumb question is there any chance there can be a bug in these generated proofs that makes it think its true? Or is it the case that as long as you verify the initial statements you are trying to prove the rest doesn't matter
Earlier quoted context omitted.
Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
I don't think Anthropic is turning a profit ;)
On a tangential note, I highly recommend this book by Simon Singh. https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)