A Critical Look at Lean4

[-]Maarten Derickx9d7

0

Really awesome post. Just some questions below because the 2% you gave is rather low and my personal estimate would easily be off by an order of magnitude (closer to 20%). So the questions below are meant to see where that difference is coming from.

"I am 2% certain that we will soon be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs." Can I ask you more precisely where your 2% is coming from? I.e. can you give some separate odds for the two closely related statements?

1. We will soon be putting huge amounts of trust into Lean4 certificates.
2. We will soon be using misaligned AI's to generate lean certificates.

I'm also curious what is meant by misaligned AI in this post, i.e. how severely misaligned does it have to be? I.e. in the context of the post there are two reasonable interpretations a) The AI is happy to exploit a kernel bug and use it to claim it found a proof of mathematical theorem. b) The AI is misaligned in such a way that it actually is likely to lead to an existential catastrophe when it is allowed to recursively self improve? Or did you have something in mind somewhere between a and b? As this chance severely depends on how misaligned one would require the ai to be.

I think interpretation a) is reasonable since the post is about lean4. While interpretation b) is reasonable since you speak about pivotal act.

Also regarding the lean certificates, will it be lean certificates of just mathematical theorems that the math community cares about. Or will it be lean certificates of statements that are relevant for alignment research?

[-]Milo Moses9d9

0

Dear Maarten,

Interpretation (b) is what I meant.

The full claim is "I am 2% certain that we will soon be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs, and that the human work we do as a community thinking about and fixing Lean4 in the next 24 months would fall under Less Wrong's classification of a pivotal act."

The fact that we'll be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs is like ~99% (or by many definitions is already happening). The part that brings the estimate down to 2% is the second part about the pivotal act.

Pivotal act is a guarded definition on Less Wrong, and I take that very seriously. It refers to "actions that will make a large positive difference a billion years later". Billions is huge! Such a distant future require significant discounting for uncertainty. That's where 2% comes in.

[-]Shuo Li12d4

1

My personal probability is that 70% of those Lean4-validated proofs are trustable. Before reading your article, my confidence was >95%.

What is your confidence in those recently Lean4-validated proofs, if you don't mind to share?

[-]Milo Moses12d8

0

My level of confidence depends strongly on a proof-by-proof basis. There's been a slew of Lean4-validated proofs lately, without a standardized level of rigor. I put it at ~40% chance that one of the recent high-visibility Lean4-formalized proofs ends up needing to be retracted, but what dominates that estimate is statement mistranslation, not soundness issues.

[-]Shuo Li12d4

0

By "statement mistranslation", do you mean that in some steps of some proofs, the proof should be proving statement A, but proved a similar statement B instead?

I asked this because LLMs usually modify my statements to generate a proof. Though I am not sure if this also happen inside those lean-formalized proofs.

[-]Mo Putera12d6

0

Yeah, for instance https://arxiv.org/abs/2610.08144. I liked the discussion in Section 4

[-]Carl Feynman11d4

1

The slippage is between the English statement of the proposition to be proven, and the Lean form of the proposition. You could leave out a clause when translating into Lean, or ask about the normal regular case when you meant to ask about the regular normal case. Since most propositions are pretty short, it's a relatively hard error to make. Once it's written in Lean, you can rely on the claimed proof being an actual proof (modulo sea monsters).

[-]Eye You12d4

1

Assuming that Lean4 is consistent, then a proof should exist and we should be able to find it

Hmm, how does this interact with Godel's Incompleteness Theorems?

[-]Milo Moses12d16

0

Godel's Incompleteness Theorem says that a sufficiently expressive theory will never be able to prove its own consistency. What you can do is prove one theory's consistency using another theory. It's perfectly fine to have a proof of Lean4's consistency within ZFC + large cardinals.

Maybe what you have in mind is something like: "How is it possible that con-leche can claim to give a proof of its own consistency"? The trick is that you start with "con-leche + strong set theory assumptions" and you conclude "con-leche is consistent". What you do NOT get is a proof of "con-leche + strong set theory assumptions is consistent". You use the stronger theory to prove the consistency of the weaker theory.

[-]taziksh12d4

0

Since Astra is flagging your requests as "cybersecurity"; maybe you could apply for OpenAI's cybersecurity program, Project Daybreak? It seems to be GPT 5.6 Sol, and not Astra, but could perhaps be helpful.

[-]Marcello5d3

0

Good points. This makes me think things like Lean4 might just be the wrong sort of target language for AI-math. One of the design constraints Lean4 was built under is to make stuff easy (or at least easier) for human authors to prove things in. But given how things have changed, the primary design consideration for AI-piloted proof languages ought to be to make sure we can trust arbitrarily long outputs without having to comb through them. OP has cast significant doubt on this for Lean4 specifically.

Given also that modern LLMs are now good enough to straight-up read and write compiled assembly code (given what various claims video game modders have made), I wonder if the right move for getting trustworthy mathematical results out of modern LLMs would instead be to implement the simplest verifier we can get away with and target that instead. The most extreme version of this would be to make a verifier for First Order Logic and the ZFC axioms (plus optionally large cardinal axioms) and just use that as the AI's compilation target. If it's just a clean implementation of FOL+ZFC itself, then there really shouldn't be any room for Sea Monsters to hide.

Of course, if we do only that, we leave the poor human mathematicians with a way bigger headache around verifying that the thing being proved is in fact the thing they want to prove. However, I imagine we could get around this by implementing a separate human-readable-definition-to-FOL+ZFC compiler (Caveat: there might still be some limits about what the theorem can actually say; maybe we can't express the sort of theorem that lives way up in type-theory-land. But if it's just a statement about the integers, or real numbers, or groups, etc. this looks doable.) This would let humans express complex math at all without drowning in pages upon pages of quantifiers.

Now granted, the definition compiler would be a more complex piece of software that can understand types and could in fact be subject to bugs just like Lean4. However, I think this would still be a substantially improved situation because said definition compiler wouldn't end up targeted by adversarial AI optimization. In this vision, human mathematicians would write down want they want to prove, compile it down to FOL+ZFC with the definition compiler and only then hand it over to the AI and demand a raw FOL+ZFC proof. Bugs in the definition-compiler would only bite us if the human mathematician chances into triggering one (while in the current situation all of Lean4 is an AI attack surface).

Caveats: There are a few ways I could imagine this trick failing. First, maybe proofs expressible in Lean4 could actually cost exponentially many tokens to say in raw FOL+ZFC (this worry makes sense if we think of the types acting as something like macros). But, it's not immediately obvious that those costs are irreducible, that the AIs wouldn't be able to find clever shortcuts through FOL+ZFC itself which don't correspond to the sorts of exponential bloat one might get when compiling something like Lean4 naively. Second, it's plausible that Lean4 ends up being an easier language for the AI to think in than raw FOL+ZFC. The assembly language results in coding are mild evidence against this. It also presumes the AI couldn't be coaxed into creating and using its own internal compiler that would compile something "easier for it to think in" into FOL+ZFC. (If either of these obstacles prove substantial the right move may then be to back off a bit and climb a little higher up the abstraction hierarchy, but only go as far as needed to make the system workable.)

[-]Blaisorblade3d1

0

We already have theorem provers in the HOL family — they assume even less than ZFC.

But a lower-level language means elaborated statements are harder to read and compare to the originals: you'll never prove a false theorem, but did you prove the right one?

[-]Blaisorblade3d1

0

I apologize for the rush, I didn't addresses your whole post. But there's quite a bit of existing debate between different theorem provers and I'm not sure I can summarize this all. "How well can we express abstract algebra in Isabelle (the most mature HOL prover)" is part of that debate and related to one of your questions.

[-]Lost Futures11d3

0

For those who are unfamiliar, the recently launched Palomar Registry project addresses a number of current Lean weaknesses. It reduces the chance of formalization gaps and proofs exploiting Lean kernel vulnerabilities, making it more reliable than Lean alone. It does not address one of the major points Milo raises though, which is the open question of whether Lean's underlying type theory is fundamentally consistent with ZFC (+large cardinal axioms).

[-]simeon_c11d3

0

Appreciate the post Milo!

I'm building a company, that I co-founded with @davidad, where we're building formal verification infra for the cyber-physical universe at large. Among others, we're building a Lean for the real-world that aims to bypass these issues by having solid theoretical foundations, that are then translated in a logic ; as a desiderata, we're also building it such that it scales to MB/GB-scale proofs, which will be required for proofs about real-world complex systems. We have made strong progress, which we will talk about more publicly in the coming months, once what we have built is mature enough for a broader community to build on it.

[-]Julien Corriveau-Trudel9d*1

0

Although the article mentions practical reasons that the Lean software might be unstable, it still has strong theoretical foundations, in a sense. Dependent type theory has been used by many theorem provers up until now (Agda, Rocq, Nuprl, and now Lean), and this fact is based on trust of this theory. Just letting you know that finding an alternative is not trivial.

From what I understand, proof theory and dependent type theory are tied together through the Curry-Howard correspondence (isomorphism).

[-]DaemonicSigil11d3

0

One of the nested inductive types described in one of the papers linked above is the RoseTree type. Its constructors are:

leaf : A -> (RoseTree A) node: (List (RoseTree A)) -> (RoseTree A)

with type parameter A: Type. So an interesting question is: Is there a way to define this type without resorting to nesting? I think the answer is yes.

The thoughts: Let's consider a simpler case: Instead of a list of arbitrary length, we'll just ask for a pair of subtrees. The resulting definition with nesting:

leaf : A -> (BinaryTree A) node: (Pair (BinaryTree A) (Binar