""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.
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. ;)
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.
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.
> 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.
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.
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.
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.
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.
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.
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
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.
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.
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_.
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.
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.
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.
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.
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.
Provides great context on this accomplishment, what it means but also doesn't mean.