At $50/M output tokens, this would have cost on the order of $300k (plus a bit for input/prefill tokens) at API rates.
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.
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
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.
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 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 and https://news.ycombinator.com/item?id=49277303
> 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.
Its like using AI to do your homework in the middle of a class. Yes, in the short term, that solves the problem of completing your homework. But it creates an entirely new problem of if you never did the homework how do you intend to pass the rest of the class or the remainder of college curriculum? A lot of cheaters ... don't.
A project has a long term path for permanent progress across an entire field. An oracle answers a question, sometimes cryptically, then progress in the field permanently ceases.
The value of a research project to determine if a Turing Machine halts with a T or a F on the tape is, to some extent, did it get a T or an F on the tape, but much more so the value is the tendrils of the rest of the field of mathematics pushing into the project at the start and then pushing out to enrich the rest of the field of mathematics at the end.
On the other hand if you have a project to run that Turing machine and see if it ever halts with a T or F as the proof, the result is completely sterile and WRT advancement of the rest of the field the actual result is kinda irrelevant. No postdoc is going to take the skills learned and move on to a position somewhere else and apply those new skills toward advancing something else in the field or describing a new goal or new way to look at the world. We'll get a popular science article about "oh it turns out the answer is indeed 'T'" and thats it. Sterile.
Personally I always thought the theorem proving turing machine would indeed terminate with a "T" and indeed it did. That's nice, and I bet the result settled a lot of bar bets. Aside from that, it will have minimal impact on progress in the field compared to the human project that's actually advancing the field.
Possibly people will be able to parse the 13 million lines of whatever into useful progress elsewhere in the field, possibly not. It'll be hard to get funding for it. OTOH its early days. Might end up useful in the end.