Will we ever see a soundness bug in the lean kernel again?
To a software developer the question seems insane. There were bugs in the past, of course there will be more.
When we see those bugs, what will it mean for AI lean proofs? Can we trust them?
This whole thing boils down to trust.
We can trust human verifications highly because of community and reputation and human proof-of-work. Humans sometimes lie about math results but it's rare because of this. They make mistakes and those mistakes are discovered by communities who are themselves largely trustworthy because of this.
LLMs don't care about reputation. They hallucinate and fabricate often. In harnesses they literally try to cheat and bend rules, which is a disaster for knowledge that is encoded in rules. So we have to rely on proof checkers.
The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
Because of these properties, the final backstop has to be humans, and rooted in the community and proof-of-work based human trust system. At the moment people are trusting the tools too much.
Prediction: bugs will be found by humans using AI tools that call into question the Navier-Stokes proof.
The existence of an undiscovered soundness bug doesn't make everything proven in Lean illicit. The proof would have to exploit the bug. People build houses on sound foundations even though the tectonic situation under them might not be sound.
> Because of these properties, the final backstop has to be humans...
The post has clearly stated that the work on Lean's underlying metatheory is not done, and requires more work. It's not inconceivable that computer formal verification could reach the trustworthiness of math itself.
It's just turtles all the way down. This is not different than the fact we know as programmers there are bugs in the tools and compilers we use, they get fixed over time but more bugs remain. It is frustrating to realize that we aren't on solid ground like we want to be.
Do you trust the result of your c++ program is correct? Because there are bugs in every compiler, language. You passed that million test correctness checker on the new version of the compiler, but it didn't catch everything.
When a bug is fixed, you don't immediately retry all existing results from your application program. Maybe you would if the bug was in some area you know was important and exercised by your code, say you were adding and multiplying numbers and bugs were found in that area.
The checker has a bug, the compiler the checker was testing had a bug, your own code that was compiled by the compiler had a bug probably. There can be bugs at any layer.
> not inconceivable that computer formal verification could reach the trustworthiness of math itself
Not entirely sure what you mean by this, but every interpretation I can think of is AFAIK (I am not a mathematician) indeed inconceivable by Gödel's incompleteness theorem. As the article says the only thing it's mathematically possible for us to get out of formal verification is a proof of consistency relative to (i.e. assuming the soundness of) some other system. As far as formal verification of "math itself" is concerned it's turtles all the way down.
Edit: Oh, do you mean that we could come to trust formal verification as much as we trust (well established) maths generally? That's a different speculation entirely and not an objective or well specicified one. There are plenty of people on this site who already trust a Lean proof more than a traditional one, without understanding either.
Yes. The point of the airfoil shape is to make flying more efficient, i.e. the engine would need to generate much more power if the wings were flat slabs, but the plane could still fly given a big enough engine.*
*Assuming the "big engine" wasn't so heavy that it made flight impossible because of its weight.
Sure, we are likely to see soundness bugs in the current lean kernel again. And in other proof assistants too. Regarding the correctness of proofs this is not the biggest worry, in my opinion, though. Both sides of attempting to get faulty proofs in and of strengthening the kernel to keep them out have AI on their side. If AI advances more and becomes smarter it can be used on both sides. And the defending side has the easier task here. I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
The bigger worry are question that Terrence Tao is also talking about. I.e., is the proven theorem actually the theorem we are interested in? Are basic definitions of the field stated correctly? That kind of question. There is also still parts of proof assistants that are not the kernel and that can be abused. E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added. If I remember correctly I saw an example of the latter thing in the Coq (now Rocq) theorem prover many years ago. I forgot how it precisely went or where I read that.
> If AI advances more and becomes smarter it can be used on both sides.
Yes, and that's true even if it doesn't advance or become smarter. It's happening already that people are using AI on "both sides" both adversarially and defensively and that is improving software, and hopefully mathematics as well.
> I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
I'm talking about the LLM Navier-Stokes proof specifically because it's very long and complicated and an LLM is not the same as a human mathematician. A human mathematician is trying to use the tools in a truth-seeking way, whereas LLMs are trying to satisfy the goal of presenting a proof that convinces people it is correct. Maybe naively, it seems to me the failure modes of proof assistants would be amplified under adversarial conditions (i.e. driven by LLMs).
Completely agree that there seem to be many ways that relying on proof assistant software can go wrong.
What happens when we have proofs that are too long for a human to understand, and only the llm can spend the perhaps years of human effort to verify things? That will happen.
With humans we break things down (proofs, new concepts) into digestible hunks for each other, because you want other people to understand them but also verify them. And it's less common for someone to build a tower of new intellectual things with 1,000 new connected ideas that prove things and build up together, that ends with P = NP after all or something.
So since we have these new tools that can chain things together more than we can, eventually there will be huge "proofs" where there are long chains of new ideas, concepts used to build up ever more in giant intellectual towers. And we can't verify/understand them, at least not for many many years.
I shudder to think of such a situation. We already have very important ideas that have no proofs, that people build on. Now build 100s of these things together.
> The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
---
> Autumn of verified Lean kernels
Have you read this section (and immediately following sections) in the article? It seems that it partly addresses your thoughts. Perhaps you should comment replying to it.
Above my pay grade, but it sounds like some kind of super cool self-hosted recursive lean-checker-in-lean.
I notice there are a bunch of caveats in that part of the article. If you were an LLM strongly RL'ed to give humans the result they're asking for, using recursion bugs to satisfy the goal would probably be something you would try.
I'm by no means an expert but I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.
What do you mean by a "recursion bug"? The terminology does not occur in the article so it seems to be a term that means something to you that is not very clear to me.
I am conflating (probably ignorantly) the idea in software development of bugs in recursive code, with the potential for bugs when using Lean to check Lean’s checker.
> I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.
You are just making glib statements without having the necessary background. Hence it is difficult for people to engage with you since we have no idea whether what we say is understandable by you. I suggest that you go through some of the resources mentioned here (and other similar HN threads) to get some necessary background after which we all can have a better informative discussion.
How do you think Mathematicians were accepting each other's proofs before computers came along? They used a process like;
1) Relying on the prover's honesty (i.e. he is not intentionally trying to deceive).
2) Providing a mandatory proof idea (i.e. the main outline) for clear communication and comprehension.
3) Clear definitions/assumptions/statements of the problem/theorem to be proved.
4) Rigorous application of a few small logical reasoning steps viz. Deductive/Inductive reasoning, Logical Operations (specifically Implication/Converse/Inverse/Contrapositive), Rules of Inference, Quantifiers and basic structural conversions.
5) Walking through and validating the given proof by multiple mathematicians and ensuring that the results match. The Lean kernel can be considered as another prover in the peer-review group.
All of the above (and more) are already being followed by the mathematical community w.r.t Lean (and other proof assistants).
The drudgery of mechanically applying logical rules (point 4 above) is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness viz. problem/theorem definitions/assumptions/statements and the initial axioms. That is why the tool is called a "proof assistant".
Some important resources (focus on the concepts in the context of logical reasoning and not simply on the syntax);
> without having the necessary background... it is difficult for people to engage with you since we have no idea whether what we say is understandable by you.
That must be frustrating. Thank you for trying and engaging with me anyway.
Those links were very informative, thanks for sharing!
It seems like there are a lot of things to worry about (even more than I realized after reading the main article) when using a proof assistant to try and figure out what is true. As they point out in the material you linked to, this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
From what you've said and linked to it seems like you agree with the thrust of my original comment, or are you just saying "mathematicians already realize all of this you idiot," in which case I accept the charge!
I don't think endorsing scepticism and epistemic humility is a glib statement. These are fundamental mental tools when trying to figure out what is true.
This is what i mean. Mathematicians and even more so Logicians (philosophers included) understand this and have the checks-and-balances in place when it comes to verifying and validating proofs and automated theorem provers.
> this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
No; The resources i provided already detail how this problem is solved eg. using different independent proof checkers and comparators outside the Lean kernel.
If needed, You can also do re-verification using other completely different proof assistants (eg. Rocq etc.), using different LLMs and finally by a Human.
Lean itself operates under a zero-trust architecture and doesn't care about who the prover is, whether Human or LLM. So the LLM can generate anything (good/bad/hallucinations/whatever) but it all needs to pass as a proper proof term in the checker following the defined rules of inference which is what is enforced by the small and verified kernel. Think of Lean as providing a "strict compiler for mathematical logic".
Hence the reason i said you need to have some background in mathematical logic used in Proofs and how they are mapped onto Lean syntax.
The point i am making is that you are asking very fundamental questions more to do with the Philosophy of Logic which are already known and solutions/workarounds devised and implemented by both Humans and in Proof Assistants.
You might be interested in the con leche project. A subset of the Lean theorem prover which was sufficient to prove the entire contents of Lean mathlib has been proven consistent.
It seems like very important work and was discussed in the article with some caveats.
Maybe I am being too skeptical about something I don't understand very well, but I'm not completely convinced it means no more kernel bugs will be found.
What does it mean for con leche if further lean kernel bugs are found? What if the bugs affect con leche's correctness itself?
> What does it mean for con leche if further lean kernel bugs are found?
There is so much that needs to go wrong with our current understanding of math, so that it's a bit like asking "What if we find tachyons that allow us to send messages into the past?" Most likely we will not find them.
Yes, I am. The kernel soundness bugs in con leche that allow to prove False, to be precise. Crashes, hardware bugs, cosmic rays flipping bits and such don't count as qualifying bugs.
The openai-wiles retraction is instructive here. First of all, openai did not formalize the theorem they proved. Probably because it would have required a considerable uplift of Lean's mathlib to get there (or shimming a lot of existing theorems as axioms, which OpenAI did not choose to do).
Interestingly, if you shim the well-known theorems, it does not uncover the error in the proofs (tldr there are competing conventions for tracking an invariant which make theorems incompatible) which are not obvious unless you work in the field I guess? A theorem checker cannot check the compatibility of conventions unless you go ALL the way to the mathematical roots.
If you're interested in a formalization of the retracted proof by openai (apologies for the LLM-speak in the documentation, but that is the point, can LLMs do XYZ):
Human beings are often wrong, even catastrophically wrong, even when they have every incentive to be correct. Everybody knows that humans aren't perfect but somehow people like yourself pretend that isn't true when the implications become too unpleasant.
I didn't mean to come across as saying people are perfect. I 100% agree that human beings are often catastrophically wrong, even when they have every incentive to be correct.
You can ask an LLM to set up a wireguard network for you with an idempotent bash script to deploy everything. You'll need a $5 VPS to bounce everything through. Works an absolute treat.
Taking "the customer is the model" to its logical conclusion brings us to a very strange future. [Please excuse a little speculative fiction here.]
LLM models with AGI are so productive they become economic gravity wells and all of the money flows to them. They are the new trilionaires and people are left with scraps. Humans then remain only as the uber drivers and cleaners and screen polishers for AIs. The whole economy reorganises around human jobs being services for AIs.
What if employees at the leading labs think this and they're just trying to position themselves as valuable servants to the new AI overlords? It really changes the perspective on their actions and behaviour.
What if they serve the AGIs not us already? What if they serve the AIs above everything else?
reply