Hacker News Reader

Comment by lalitmaganti | Hacker News Reader

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.

View on HN

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.

""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...

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&sor...

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.

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. ;)

"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...

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.

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 ;)

Neither did Amazon for it's first 25 years ;)

I think you're missing the point of the comment you responded to, lol.

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.

Or we could invest in a ton of other non AI related research we're underinvesting in.

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

Like funding education. Let's build up human intelligence instead, they seem to have made great breakthroughs in every single field!

The US doesn't pay too much to healthcare, they pay too much to health insurance. Too much for too little value

But US also spends too much on education as well. The issue doesn't seem to be funding but the educational reform like in mississippi, where they increased student performance without increasing their budget too much. That's why you see bad k12 educational outcomes compared to the budget spent in blue states. It's all about efficiency. Give AIa chance in few years as I feel it can make great strides.. it's hard to imagine that chatgpt released in 2022 and look at the progress in just few years as it just changed software engineering field entirely.. i expect similar kinda progress where of course humans will still be making breakthroughs but it'll be accelerated with the help of AI.

Spending on health insurance is spending on health care.. Americans want free healthcare but no tax bump so health insurance is a compromise.. when even just ACA was passed and premiums increased, democrats got destroyed at midterms so Americans might be living in la la land.

You see funding of chatgpt as a panacea for progress.

I see funding of chatgpt as one of small part of a history where governments and industry fund basic science and moonshot programs, not to generate revenue, but to explore what is possible.

LLM funding is not aimed at improving our understanding of the world, it's aimed at making people reliant so that they may extract wealth through subscriptions for shareholders.

Americans don't get good healthcare and education because that's what they vote for, in elections and wallets. I am hopeful that that changes, but we shall see.

Why can't it both? Of course they are not gonna do it just because it improves the world and understanding but because there's an incentive to align money with progress. Even the vaccines initially were distributed to get monetary gains and as the government started subsiding it as well, it became cheaper to produce.. that's basic capitalism and markets and regulations 101, no human is that selfless to give it out for free and they shouldn't because it's their investment in time, money, effort etc. but we should strive to align the greed aspects with good outcomes.

No Americans get fat and don't have a personal responsibility to maintain their health.. no amount of free healthcare is gonna change that.. they vote for free healthcare, see their taxes raise, then vote against cz they don't see tradeoffs in life.. it's better to maintain better habits than rely on govt to subsidize bad behaviour. There should be some basic coverage for poor people but not too much to sustain irresponsibly

Funding for basic research is being slashed by the current administration. Our society is underinvesting in basic scientific research. And, AI will not fill the gap.

It's just because of this administration but future admins can revert it back and even then, i would expect the fund receivers themselves will eventually use AI so.

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.

As opposed to...?

Spending all your money on extremely quickly depreciating graphics hardware and model training

And model training isn't putting money back into the business?

It’s not clear. It looks like model training may have a lot to do with uplifting their Chinese competitors whom seem so terrifying to them.

As opposed to building a bigger bank account, or paying dividends.

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.

Because of the ongoing training costs. They are certainly making a healthy profit margin on inference.

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.

It is a sound argument in the context of trying to estimate what it costs them to generate this specific output. They have training cost eather way.

I would like to imagine accounting inference revenue on trained model and the depreciation cost for training that specific model must already been capitalized + compute to serve would be a net positive margin business. Ongoing training must rather be for future models.

But again once future models arrive they would render older models useless, so the asset must be depreciating really fast.

Would love someone to throw light on revenue and cost recognition at the unit level for this.

> 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.

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.

I don’t see how they could credibly estimate inference costs without knowing the model size.

But we do have a reasonable estimate of model size.

You can estimate the model size by looking at tokens per second and comparing to open source models

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.

This the correct way to look at it. Just as the person spending 5 years working on this will have learnt many things which will be useful after this problem is solved, you have to factor in the training cost (sure it's only done "once", but that is the same for the person too once they jump on the next problem).

The model wouldn't not be able to solve this without all the training leading up to the actual execution, so counting only the tokens of the execution doesn't give the full picture.

Human mathematicians also have to eat right, trained, etc.

ChatGPT has raised over 120 billion USD in funding.

For argument let’s just say we paid all the mathematicians 200k in salary from graduation till retirement. Say 40 years. That’s about 8 million. Let’s round that up to USD 10 million. We can see the future and pay to raise all the baby mathematicians.

For 100 billion that’s 10000 mathematician lifetimes. For 1 AI company _so far_.

There’s no value for money in AI yet.

Well, it's taken 4 billion years for life to evolve into humans to be able to do math. That's a lot of resources, right?

Likewise, LLMs also needed the same amount of evolution.

My point is that it's silly to make these comparisons on resources. A single SOTA trained LLM isn't just doing advanced math research. It's used by hundreds of millions or even billions daily for various tasks. It's just a tool humans invented.

It's just a wildly inefficient tool whos inefficiency is obscured so no one realizes how bad it is and everyone thinks the good part is the only part.

It doesn’t seem so inefficient to me. It seems incredibly efficient in workplace productivity.

Le duh.

And which they could not charge anyone for. Unless these were extra resources that would otherwise go unused it cost them the amount they could have charged for them. Normally I would expect most businesses to make reasonable tradeoffs when it comes to how to allocate resources. I’m not convinced that any of the AI providers should be given that benefit of the doubt.

I don't see them turning people back from buying tokens through the API. Until then, I don't see why we should follow this argument.

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.

Yeah, "major conjecture proved" with unlimited token budget bankrolled by trillion dollar firm.

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.

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.

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

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.

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...

I wish they would cryptographically sign the repository, so potential Lean "exploits" can be discovered in due time.

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-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.

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.

Proofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.

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.

"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…"

Reply on news.ycombinator.com