411–420 of 523 posts
Earlier quoted context omitted.
With the size of the proof object, a potential buffer overflow comes to mind.
Buffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it. I’d wager a million gazillion bucks that this is not the case.
The thing is: LLMs are not grounded in reality enough as much as we are. Using Lean is exactly what that is: grounding LLMs in reality.
We have (at least) 30 FPS vision, and can detect 5 ms audio delays, we do that in real-time. LLMs have access to some images and large amounts of text. Their propensity is to predict the next token. So the propensity to be additive and just say something (aka predict the next token) is higher than predicting something to stop.
If LLMs would have: - 30 FPS vision - similar hearing ability - an ability to feel their lived experience - consequences to their "life"
They'd be making more intelligent decisions than they are doing now. Simply because they have more context.
Because in this sense, we have a lot more context than LLMs. Yet, I see people sometimes treating them as if they are at the same level as humans because their intelligence is similar. And that might be true, but where they get their data from is vastly different. Given our tasks, they are at a disadvantage. They need to sense more of reality.
Have fun sharing the room with these digital intelligences. Given the topics they can consume, they are already better generalists than any individual. I might be wrong of course, I'd love to meet any individual that's a better generalist than an LLM.
Hmm kind of funny, some years ago someone claimed LLMs can do math, and I replied if it could prove fermants theorem: https://news.ycombinator.com/item?id=33176996#33177939 > Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2. > > Shifting the goal posts a bit, aren't we? I guess the goalposts did change a bit, and in a pretty short time.
So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That…
The answer is we don't really know [0]: > In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid However it's a bit dif…
What are the chances that a very large C program uncovers a bug in the C compiler?
We'll increasingly observe announcements of this kind as AI tooling scales. As impressive as agentic coding is, it pales in comparison to the value proposition of medical, mathematical, and physics research. I optimistically expect to witness the advent of a global 'panacea' in my lifetime thanks to AI's efforts. Cost effective large scale genetic engineering, a cure for every disease, potentially even a cure for agi…
How does that work for drugs? We can’t let AIs make millions of test drugs and try them out on people.
13M LoC, are we sure it didn't exploit any latent issues in the lean proof system?
That must have slipped through Kevin Buzzard's review, which is not entirely unplausible with 29500 theorems to verify... I think they should spend another few billion tokens and let agents try to disprove any of those statements or links between them. Then I'd be a lot more convinced.
They should let AI work on it until the proof fits in the margin of a page.