5 ms·

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://

I suggest also reading Kevin Buzzard's blog post which was just posted: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h... Provides great context on this accomplishment, what it means but also doesn't mean.

faitswulff 1mo ago
I’m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.
- aquafox 1mo ago
  We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)
deleted 1mo ago
[deleted]
BeetleB 1mo ago
"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…" Gives you an idea of the scale...
- sebzim4500 1mo ago
  It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
  - _aavaa_ 1mo ago
    Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
    - alch- 1mo ago
      I don't think Anthropic is turning a profit ;)
      - dist-epoch 1mo ago
        Neither did Amazon for it's first 25 years ;)
        caughtinthought 1mo ago
        I think you're missing the point of the comment you responded to, lol.
        CaptWorld 1mo ago
        Regardless the profit margin as a talking point seems to be bad as AI as a tech might never be reversed whether anthropic failed or succeeded. Indeed it's imperative we subsidize AI companies and tech to make them explore more solutions to scientific problems which has a downstream effect on human flourishing.
        oblio 1mo ago
        Or we could invest in a ton of other non AI related research we're underinvesting in.
        CaptWorld 1mo ago
        Like? I feel breakthroughs that can be found via AI might help us more in the long term where even previously non AI fields can be helped by AI. So you have specific non AI research in mind that we're underinvesting in? Because the USA is already spending crazy anyway for healthcare and I don't feel like funding is the issue but better incentives, reforms etc
        1mo ago
- UltraSane 1mo ago
  I burned $70 on fable 5.1 Max in about 2 hours. I suggest never using fable 5.1 on higher than High reasoning unless someone else is paying for it.
  - paulpauper 1mo ago
    Yeah, "major conjecture proved" with unlimited token budget bankrolled by trillion dollar firm.
- iterateoften 1mo ago
  How many previous attempts with other models failed or on other problems. Perhaps this is $300k out of $100M or $1B of total budget just breadth first searching theorems in math and all the failed attempts conveniently don't get mentioned.
dang 1mo ago
Thanks! I've added that link to the toptext. I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-theorem https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.
- deleted 1mo ago
  [deleted]
- jonesn11 1mo ago
  ""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)."" lol if you say so buddy...
  - dang 1mo ago
    Hey! If you know more than others (which I'm guessing you do), that's great - but in that case can you please share some of what you know, so the rest of us can learn? If you only post a putdown, it just makes the thread mean and the rest of us don't get to learn anything. https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sort=byDate&type=comment&query=share%20know%20learn%20by:dang https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...
blondie9x 1mo ago
"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…"
fspeech 1mo ago
To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.
- fspeech 1mo ago
  The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main/tools/docs-site/README.md https://github.com/anthropics/fermats-last-theorem/blob/main...
  - DoctorOetker 1mo ago
    I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
    - fspeech 1mo ago
      I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-frey-package-wlog.md https://github.com/htzh/flt_for_human/blob/main/math/001-fre... which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
      - DoctorOetker 1mo ago
        I don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages). The Lean system has already experienced soundness bugs. The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this. I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.
qnleigh 1mo ago
I wonder what he's feeling about this. Formalizing Fermat's last theorem was a huge undertaking, and has been a big part of his career for some time. Now the announcement has been made, and even if there is more work that he wants to do, he has in some ways been scooped by an LLM. Fortunately he is a very well-established mathematician, so career-wise he will likely be fine. But if an early-career mathematician gets scooped this badly it could be career-ending.
- someguynamedq 27d ago
  Being in a career that is scoopable by a dev with no special expertise running an agent is career ending
hn_throwaway_99 29d ago
Regarding "what it doesn't mean", when I read that I thought there would be some sort of limitation on what Claude could do in the realm of proof autoformalization, but that's not really true. All the "what it doesn't mean" stuff that Kevin mentions is basically just stuff that he thinks Anthropic won't get around to because it's not that important to them, but they certainly could if they desired: > 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). What I'm saying is that if you thought there were still some scraps in this domain where humans still had some superior capabilities, that does not seem to be the case.

faitswulff 1mo ago

I’m not very good at mathematics, but it seems like Kevin should take his girlfriend on trips more often for the good of all mathematicians.

aquafox 1mo ago
We should start a gofundme to send him 2 months to a remote tribe in the Amazon. Chances are, we see the Riemann hypothesis and twin prime conjecture proven. ;)

deleted 1mo ago

[deleted]

BeetleB 1mo ago

"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…" Gives you an idea of the scale...

sebzim4500 1mo ago
It sounds plausible they spent more, given the output tokens (6 billion of them) would cost $300k at API prices and presumably there will have been many more input tokens than output tokens.
- _aavaa_ 1mo ago
  Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
  - alch- 1mo ago
    I don't think Anthropic is turning a profit ;)
    - dist-epoch 1mo ago
      Neither did Amazon for it's first 25 years ;)
      - caughtinthought 1mo ago
        I think you're missing the point of the comment you responded to, lol.
        CaptWorld 1mo ago
        Regardless the profit margin as a talking point seems to be bad as AI as a tech might never be reversed whether anthropic failed or succeeded. Indeed it's imperative we subsidize AI companies and tech to make them explore more solutions to scientific problems which has a downstream effect on human flourishing.
        oblio 1mo ago
        Or we could invest in a ton of other non AI related research we're underinvesting in.
        CaptWorld 1mo ago
        Like? I feel breakthroughs that can be found via AI might help us more in the long term where even previously non AI fields can be helped by AI. So you have specific non AI research in mind that we're underinvesting in? Because the USA is already spending crazy anyway for healthcare and I don't feel like funding is the issue but better incentives, reforms etc
        1mo ago
UltraSane 1mo ago
I burned $70 on fable 5.1 Max in about 2 hours. I suggest never using fable 5.1 on higher than High reasoning unless someone else is paying for it.
- paulpauper 1mo ago
  Yeah, "major conjecture proved" with unlimited token budget bankrolled by trillion dollar firm.
iterateoften 1mo ago
How many previous attempts with other models failed or on other problems. Perhaps this is $300k out of $100M or $1B of total budget just breadth first searching theorems in math and all the failed attempts conveniently don't get mentioned.

dang 1mo ago

Thanks! I've added that link to the toptext. I'd really like to make it the top link (and relegate https://www.anthropic.com/research/formalizing-fermats-last-theorem https://www.anthropic.com/research/formalizing-fermats-last-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.

deleted 1mo ago
[deleted]
jonesn11 1mo ago
""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)."" lol if you say so buddy...
- dang 1mo ago
  Hey! If you know more than others (which I'm guessing you do), that's great - but in that case can you please share some of what you know, so the rest of us can learn? If you only post a putdown, it just makes the thread mean and the rest of us don't get to learn anything. https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sort=byDate&type=comment&query=share%20know%20learn%20by:dang https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...

blondie9x 1mo ago

"I was given £1M to run my project over 5 years; Anthropic took only 11 days but I do wonder if they spent more money…"

fspeech 1mo ago

To really read the proof, clone the repo and drop the root index.html into your browser and enjoy. Due to the large amount of files in a directory Github won't serve the .lean files in Theorems/ beyond A. Github preview won't work with the htmls beyond the few top level docs either.

fspeech 1mo ago
The webpages are entirely generated without a binary build (a build from scratch is quite daunting as stated in the project readme) of Lean artifacts. See https://github.com/anthropics/fermats-last-theorem/blob/main/tools/docs-site/README.md https://github.com/anthropics/fermats-last-theorem/blob/main...
- DoctorOetker 1mo ago
  I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.
  - fspeech 1mo ago
    I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-frey-package-wlog.md https://github.com/htzh/flt_for_human/blob/main/math/001-fre... which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
    - DoctorOetker 1mo ago
      I don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages). The Lean system has already experienced soundness bugs. The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this. I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.

qnleigh 1mo ago

I wonder what he's feeling about this. Formalizing Fermat's last theorem was a huge undertaking, and has been a big part of his career for some time. Now the announcement has been made, and even if there is more work that he wants to do, he has in some ways been scooped by an LLM. Fortunately he is a very well-established mathematician, so career-wise he will likely be fine. But if an early-career mathematician gets scooped this badly it could be career-ending.

someguynamedq 27d ago
Being in a career that is scoopable by a dev with no special expertise running an agent is career ending

hn_throwaway_99 29d ago

Regarding "what it doesn't mean", when I read that I thought there would be some sort of limitation on what Claude could do in the realm of proof autoformalization, but that's not really true. All the "what it doesn't mean" stuff that Kevin mentions is basically just stuff that he thinks Anthropic won't get around to because it's not that important to them, but they certainly could if they desired: > 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). What I'm saying is that if you thought there were still some scraps in this domain where humans still had some superior capabilities, that does not seem to be the case.