471–480 of 531 posts
Earlier quoted context omitted.
maybe that's because the doom and gloom is the transparently correct outcome?
Why? Even communists weren't this doomed and were actively rooting for it to solve the economic calculation problem which ai might take us to. People are just pessimistic in general ig
This is probably the best and succinct explanation of what’s coming.
Earlier quoted context omitted.
To me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean. What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs t…
> What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand. The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be tr…
The source article does acknowledge this isn't a replacement for human analysis, but they seem to imagine a vision of mathematical research where there's a bunch of AIs running around proving random things and formalizing them into opaque Lean proofs nobody ever has to read. I'm skeptical whether there's any value in doing that, and to the extent that there is I'm pretty confident it looks more like proving certain directions aren't fruitful for further investigation.
Earlier quoted context omitted.
They didn't die of senescence.
The argument was that senescence is as natural as child mortality, and thus naturalness is not a reason not to fight against it.
No matter what standard of care you receive, senescence will gradually kill you even with therapies or treatments to slow it. It's a part of the built-in natural lifecycle that humans can't avoid; it's not analogous to the treatment of incidental injury like pneumonia or sepsis.
I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty cool.
What else is interesting is how they staged this problem : (a) maintain an explicit DAG/roadmap of sub-goals rather than one flat prompt, (b) separate statements from proofs so many agents can work on different nodes without stepping on each other, (c) keep a natural-language index alongside the formal one so search/reuse works... I feel like this is the future of long horizon agents and how you can do work that's making the most of every agent. This approach will likely be baked into the next versions of coding harnesses
Earlier quoted context omitted.
> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?
It is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct. This is how the theorem for FLT looks in the particular proof we discuss here: theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of…
Earlier quoted context omitted.
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 abo…
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) 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
Note that this proof while impressive does not add any value to mathematics as a human pursuit. But it does show we can throw these LLM beasts at much gnarlier problems than we could have imagined previously. Maybe even formally verify papers the day they are posted? I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty…
I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
Earlier quoted context omitted.
They said 6 billion tokens, which isn't as much as I thought it might be.
Am I doing my napkin math correct? The post says it's using a model comparable to Fable 5.1, which is $50 per million output tokens. So this is ~$300K? Surely an over-estimate due to caching.
Note that this proof while impressive does not add any value to mathematics as a human pursuit. But it does show we can throw these LLM beasts at much gnarlier problems than we could have imagined previously. Maybe even formally verify papers the day they are posted? I'd love to see an e2e compiler or OS kernel verification or Full-stack chip design with formal equivalence checking at each stage that would be pretty…
> Note that this proof while impressive does not add any value to mathematics as a human pursuit. I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
The relevant quote is
> one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?"
And later
> But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided by any human expert in the field X resides in, has created an unprecedented divergence between the production of answers, and the production of insight, to the point where the two questions have become _negatively correlated_:
Earlier quoted context omitted.
There is no way Fermat could have fit that in the margin. Definitely vindicated.
I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.
In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday.
Enjoyed that idea. Not sure how true but it was enjoyable.