> a team of agents completed the proof in a little under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.
At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
And human salaries for those who worked on the prover harness etc. which isn't just standard Fable.
It also uses Prove2Me, which uses a graph like previous automated theorem provers. A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Now they have it in writing.
> A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used.
> Now they have it in writing.
Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this
But also achievable on a $150/mo (CAD) Max 5 subscription (I currently have 11.6B tokens in the last 30 days) according to /usage. It doesn’t break down input vs. output tokens as far as I can tell.
~10B tokens a month is pretty typical overall input/output usage from my own experience and other developer accounts I've seen
It's 6B output tokens, as stated by the blog post.
When writing software with Codex 95+% of tokens are cache, I would assume the same in your case (if you also used it for coding).
What would it cost to make a team of mathematicians do the same?
The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.
Buzzard was given 1kk GBP and 5 years and his goal I think wasn't the full thing like Anthropic did. So much more cash and orders of magnitude more time. The proof is about 5x the whole Mathlib library which was developed over many years by dozens of people.
It's true that his goal was not the full thing, but it was also not merely a Lean verified proof. From the blog post linked in the toptext:
> 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.
1kk? Why not say 1M?
You mean why not say £ 1MM?
More importantly how many years it would take.