Formalizing Fermat's Last Theorem

455 points by jlebar 6 hours ago

https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...

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

Provides great context on this accomplishment, what it means but also doesn't mean.

dang - 4 hours 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-... to the toptext) since HN has been tracking the work of https://news.ycombinator.com/user?id=kevinbuzzard for a long time and we're big fans. But I guess that would be overkill.
faitswulff - 6 hours 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 - 5 hours 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. ;)
BeetleB - 5 hours 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 - 5 hours 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_ - 5 hours ago
    
    Unlikely, api pricing includes a healthy profit margin (as near as we can tell from the outside) which they wouldn’t charge themselves.
    
    mbesto - 4 hours ago
    
    > healthy profit margin (as near as we can tell from the outside)
    Ugh we still don't know if this is true and it's nearly impossible to calculate without a full understanding of the real CAPEX cycle. Stop spreading these rumors until we know for sure.
    
    bryanlarsen - 3 hours ago
    
    SemiAnalysis estimates their profit margin to be 70%. To be losing money on inference implies that their costs are almost 4X higher than SemiAnalysis has calculated. That's not credible.
    
    p-e-w - an hour ago
    
    I don’t see how they could credibly estimate inference costs without knowing the model size.
    
    FuckButtons - 42 minutes ago
    
    But we do have a reasonable estimate of model size.
    
    2muchcoffeeman - 2 hours ago
    
    The token price seems like a poor measure.
    Building the LLM that could do this work in 11 days cost multi billions.
    The economics probably only make sense if LLMs prove to be a benefit to almost everyone in a way we can all accept.
    Otherwise this cost a lot more than we’d otherwise pay. It was incredibly fast though. But we all know: cost, speed, quality. Pick two.
    
    alch- - 4 hours ago
    
    I don't think Anthropic is turning a profit ;)
    
    _aavaa_ - 4 hours ago
    
    Whether on net they turn a profit as company overall is neither here nor there.. My point is that they are selling API tokens at a profit (or if being pedantic, then at a price higher than the cost to serve them ignoring research costs). And that that price is got a healthy margin which they don't charge themselves.
    
    irthomasthomas - 4 hours ago
    
    Because of the ongoing training costs. They are certainly making a healthy profit margin on inference.
    
    Philip-J-Fry - 3 hours ago
    
    Never really a sound argument.
    It's like having new solar panels installed every week. Sure you're "profitable" on the $0.20/kWh you're selling your "free" energy at when you ignore the cost of the solar panels you're buying every week.
    
    dist-epoch - 4 hours ago
    
    Neither did Amazon for it's first 25 years ;)
    
    btilly - an hour ago
    
    Amazon didn't make a profit because they were reinvesting money into starting new lines of business.
    Basically there was a choice between taking the money, and growing. They chose growth.
    
    chpatrick - 42 minutes ago
    
    As opposed to...?
    
    caughtinthought - 4 hours ago
    
    I think you're missing the point of the comment you responded to, lol.
    
    CaptWorld - 4 hours 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 - 4 hours ago
    
    Or we could invest in a ton of other non AI related research we're underinvesting in.