5 ms·

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

by davmre 14d ago

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

3192987 14d ago
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.
- logicprog 14d ago
  > 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
  - 123aHgf 14d ago
    Wrong. AlphaProof is much older, used Lean and a tree search for tactics just like ACL2. They all steal from ACL2 without attribution in the current publication boiler room atmosphere. They get away with it because the AI Cult has information and publication dominance. There was a brief period that used only language for toy IMO problems, but for serious work like FLT they apparently reverted to established approaches.
  - porridgeraisin 13d ago
    Literally many previous instance used one. Right from alphaevolve onwards. I'm not some "LLM is just a next token predictor guy" (GP seems to have a thing against LLMs), but to use LLMs properly you genuinely do need a grounded verifier and a planner. Coding harnesses for example are exactly that. For some plans, you can AR generate the search tree and that's what subagents being planned around by high level (LLM)agents and such are. Coding agents even with subagents are imperfect even on verifiable tasks only because of that. If you can put a human to simply guide it, it becomes a full system. This is what we all do today whenever we use codex. It's not something that is "never done before". I also don't subscribe to the purist view which is taken by GP. I prefer to think in terms of concentration inequalities. P(failure rate > r) < epsilon. You get different levels of autonomy for different values of r for the planner and verifier each. If you have a good planner and a good verifier, r is very very small and it's super useful. Autonomy at a given r comes from how much of the planner and how much of the verifier is automated at that r. All levels of autonomy are economically useful. Many values of r are economically useful. In this case of FLT, the verification was entirely automated using lean, and it is correct upto lean compiler bugs (so a very small r). The planner was essentially a maintained graph (afaik. Prove2me doesn't use A* or any heuristic/evolutionary methods to limit or prune the frontier), AND importantly - I'm not seeing anyone on HN mention this - some human nudges, literally, which nodes to open. The way to make AI systems more useful is to build great verifiers and great planners, which is what many companies and startups are doing. LLMs are already really really good proposers due to excellent generalization (to be pedantic, multiple stacked specialisations), especially MoE models, making them amenable to proposing at every point in a vast search tree without any adaptation. Yes, it is possible to do complex tasks purely AR, so long as you can AR simulate the search, which in the case of LLMs corresponds to verbalising the search tree[4]. This is trivially true. Can this be useful? Yes. Can a millenium prize problem be solved purely AR? Sure. It's a hard problem for humans, there is no reason it has to be difficult to reach in the conditional distributions of every future LLM. In the trivial limit, an LLM trained on the solution 100% you can sample it out. An LLM 2 generations behind that may have it at p=0.001, entirely reachable given a planner, but probably not AR. An LLM 1 generation behind may have it at p=0.05, plausibly reachable purely AR. But the key question is: is `r` smaller or larger if you have a planner versus not? The answer there is obvious. Second, if you have a threshold `r` that decides usefulness, is the set of things you can autonomously do under that threshold higher with planners and verifiers? Again the answer is an obvious yes. Copy pasting code from chatgpt repeatedly is worse than using a coding harness where it gets grounded feedback, LLM weights kept constant. Keeping the history of things and the overall plan that worked fixed and isolating LLMs to do subtasks is better than developing a whole database in one continuous context. In some cases, the overall plan "tree" can itself be entirely verbalised, but most commonly there is human modifications/steering. Can pure-LLM coding harnesses with just verifiers one shot most e commerce sites including planning? Yes. But we want to do more with it than e commerce sites. Will it keep improving thus enabling us to do more and more complex things? No obvious reason for a fixed limit to exist in theory[1]. But at any point on the progress curve, using it with a harness always gives better results versus not. Concretely, with fable 5.1, using it without a harness could not prove FLT in reasonable token budgets [3]. However, it is possible for say, idk, GPT9, trained on this, to verbalise this whole proof tree, and also potentially generalize it to another open problem, purely AR, in a reasonable token budget[2]. This was how we got from gsm8k to FLT in the first place. It's not a binary "AR is useless" "AR is all you need". [1] the limits are mostly economic, and time is itself a limit, see https://news.ycombinator.com/item?id=49161078 https://news.ycombinator.com/item?id=49161078 Tl;dr diminishing returns of test time scaling. Noam brown also has a piece about this. [2] if it's too many tokens that we run out of time or money literally, that is the limit described in [1]. It is not linear or constant scaling necessarily as described again in [1]. [3] [2] is why we have to add token budgets as another axis apart from r and the autonomy level. [4] And, the distribution conditioned on that verbalisation must be amenable to sampling the verbalisation of the execution of the plan from. This is not a given, see https://arxiv.org/abs/2504.09762 https://arxiv.org/abs/2504.09762 and https://news.ycombinator.com/item?id=49277303 https://news.ycombinator.com/item?id=49277303
- ddosmax556 12d ago
  Your comment appears to imply that the fact that LLMs used prove2me makes their accomplishment in any way less powerful. But consider that we just witnessed an AI system generate an automated proof that was previously unthinkable within 11 days and 300k+ of money. What tools were used along the way is kind of irrelevant, would you not say?
jensgk 14d ago
What would it cost to make a team of mathematicians do the same?
- dist-epoch 14d ago
  More importantly how many years it would take.
- nearbuy 14d ago
  The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.
- margorczynski 14d ago
  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.
  - jascination 14d ago
    1kk? Why not say 1M?
    - emil-lp 14d ago
      You mean why not say £ 1MM?
  - traes 14d ago
    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.
tonyarkles 14d ago
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.
- wolttam 14d ago
  ~10B tokens a month is pretty typical overall input/output usage from my own experience and other developer accounts I've seen
- dist-epoch 14d ago
  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).
- fspeech 14d ago
  It's 6B output tokens, as stated by the blog post.
deleted 14d ago
[deleted]
deleted 14d ago
[deleted]

by davmre 14d ago

3192987 14d ago

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.

logicprog 14d ago
> 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
- 123aHgf 14d ago
  Wrong. AlphaProof is much older, used Lean and a tree search for tactics just like ACL2. They all steal from ACL2 without attribution in the current publication boiler room atmosphere. They get away with it because the AI Cult has information and publication dominance. There was a brief period that used only language for toy IMO problems, but for serious work like FLT they apparently reverted to established approaches.
- porridgeraisin 13d ago
  Literally many previous instance used one. Right from alphaevolve onwards. I'm not some "LLM is just a next token predictor guy" (GP seems to have a thing against LLMs), but to use LLMs properly you genuinely do need a grounded verifier and a planner. Coding harnesses for example are exactly that. For some plans, you can AR generate the search tree and that's what subagents being planned around by high level (LLM)agents and such are. Coding agents even with subagents are imperfect even on verifiable tasks only because of that. If you can put a human to simply guide it, it becomes a full system. This is what we all do today whenever we use codex. It's not something that is "never done before". I also don't subscribe to the purist view which is taken by GP. I prefer to think in terms of concentration inequalities. P(failure rate > r) < epsilon. You get different levels of autonomy for different values of r for the planner and verifier each. If you have a good planner and a good verifier, r is very very small and it's super useful. Autonomy at a given r comes from how much of the planner and how much of the verifier is automated at that r. All levels of autonomy are economically useful. Many values of r are economically useful. In this case of FLT, the verification was entirely automated using lean, and it is correct upto lean compiler bugs (so a very small r). The planner was essentially a maintained graph (afaik. Prove2me doesn't use A* or any heuristic/evolutionary methods to limit or prune the frontier), AND importantly - I'm not seeing anyone on HN mention this - some human nudges, literally, which nodes to open. The way to make AI systems more useful is to build great verifiers and great planners, which is what many companies and startups are doing. LLMs are already really really good proposers due to excellent generalization (to be pedantic, multiple stacked specialisations), especially MoE models, making them amenable to proposing at every point in a vast search tree without any adaptation. Yes, it is possible to do complex tasks purely AR, so long as you can AR simulate the search, which in the case of LLMs corresponds to verbalising the search tree[4]. This is trivially true. Can this be useful? Yes. Can a millenium prize problem be solved purely AR? Sure. It's a hard problem for humans, there is no reason it has to be difficult to reach in the conditional distributions of every future LLM. In the trivial limit, an LLM trained on the solution 100% you can sample it out. An LLM 2 generations behind that may have it at p=0.001, entirely reachable given a planner, but probably not AR. An LLM 1 generation behind may have it at p=0.05, plausibly reachable purely AR. But the key question is: is `r` smaller or larger if you have a planner versus not? The answer there is obvious. Second, if you have a threshold `r` that decides usefulness, is the set of things you can autonomously do under that threshold higher with planners and verifiers? Again the answer is an obvious yes. Copy pasting code from chatgpt repeatedly is worse than using a coding harness where it gets grounded feedback, LLM weights kept constant. Keeping the history of things and the overall plan that worked fixed and isolating LLMs to do subtasks is better than developing a whole database in one continuous context. In some cases, the overall plan "tree" can itself be entirely verbalised, but most commonly there is human modifications/steering. Can pure-LLM coding harnesses with just verifiers one shot most e commerce sites including planning? Yes. But we want to do more with it than e commerce sites. Will it keep improving thus enabling us to do more and more complex things? No obvious reason for a fixed limit to exist in theory[1]. But at any point on the progress curve, using it with a harness always gives better results versus not. Concretely, with fable 5.1, using it without a harness could not prove FLT in reasonable token budgets [3]. However, it is possible for say, idk, GPT9, trained on this, to verbalise this whole proof tree, and also potentially generalize it to another open problem, purely AR, in a reasonable token budget[2]. This was how we got from gsm8k to FLT in the first place. It's not a binary "AR is useless" "AR is all you need". [1] the limits are mostly economic, and time is itself a limit, see https://news.ycombinator.com/item?id=49161078 https://news.ycombinator.com/item?id=49161078 Tl;dr diminishing returns of test time scaling. Noam brown also has a piece about this. [2] if it's too many tokens that we run out of time or money literally, that is the limit described in [1]. It is not linear or constant scaling necessarily as described again in [1]. [3] [2] is why we have to add token budgets as another axis apart from r and the autonomy level. [4] And, the distribution conditioned on that verbalisation must be amenable to sampling the verbalisation of the execution of the plan from. This is not a given, see https://arxiv.org/abs/2504.09762 https://arxiv.org/abs/2504.09762 and https://news.ycombinator.com/item?id=49277303 https://news.ycombinator.com/item?id=49277303
ddosmax556 12d ago
Your comment appears to imply that the fact that LLMs used prove2me makes their accomplishment in any way less powerful. But consider that we just witnessed an AI system generate an automated proof that was previously unthinkable within 11 days and 300k+ of money. What tools were used along the way is kind of irrelevant, would you not say?

jensgk 14d ago

What would it cost to make a team of mathematicians do the same?

dist-epoch 14d ago
More importantly how many years it would take.
nearbuy 14d ago
The Kevin Buzzard post linked at the top says they budgeted £1M over 5 years for a smaller proof.
margorczynski 14d ago
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.
- jascination 14d ago
  1kk? Why not say 1M?
  - emil-lp 14d ago
    You mean why not say £ 1MM?
- traes 14d ago
  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.

tonyarkles 14d ago

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.

wolttam 14d ago
~10B tokens a month is pretty typical overall input/output usage from my own experience and other developer accounts I've seen
dist-epoch 14d ago
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).
fspeech 14d ago
It's 6B output tokens, as stated by the blog post.

deleted 14d ago

[deleted]

deleted 14d ago

[deleted]