What mathematicians should know about the Lean Theorem Prover: reliability & AI
terrytao.wordpress.com
[hidden]
This is lamentable.
[hidden]
[7 comments hidden]
Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.
[5 comments hidden]
I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?
[2 comments hidden]
IE a proof can be true, rigorous, and not at all what was asked for.
[hidden]
In the process of formalizing, you find bugs, you find gaps, you find ways to fill those in. Maybe you rewrite part of the proof. Maybe you didn't quite wind up with the same result. Perhaps your theorem has some new conditions or something.
Was the original paper true? Maybe. But that isn't what you verified. What you verified is almost surely true though. So you take the win, and move on.
[hidden]
The Lean kernel did its job verifying that the compiled code was logically consistent, but the code wasn't proving what the English paper claimed.
[2 comments hidden]
Another related and more approachable paper on the evolution of Type Theory and its relation to Set/Category theories is Types, Sets and Categories by John Bell.
Finally also see, Typed Lambda Calculus / Calculus of Constructions by Helmut Brandl for an excellent book-length but concise overview of CoC/CIC.
IMO, the above is required reading to understand theorem provers and proof assistants. In particular, Brandl's work is a must-read.
[hidden]
https://github.com/AndrasKovacs/elaboration-zoo
I've also got an incomplete project that aims to present a more expanded set of implementations then the elaboration zoo: https://github.com/solomon-b/lambda-calculus-hs
chr15m[10 comments hidden]
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.
jhanschoo[3 comments hidden]
---
> 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.
chr15m[2 comments hidden]
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.
jhanschoo[hidden]
plesiv[3 comments hidden]
> 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.
chr15m[hidden]
Yes, correct. The proofs would have to be checked to make sure they don't exploit the bug.
> computer formal verification could reach the trustworthiness of math itself.
Yes, it could. I don't think that is currently the case.
omnicognate[hidden]
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.
carodgers[2 comments hidden]
chr15m[hidden]
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?
cjfd[hidden]
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.