Type theory of lean 4

Stream: lean4

[Horatiu Cheval]

I've been wondering about this question, but I don't know enough about this in order to answer myself. Does Lean 4 introduce any modifications to Lean 3 at the level of the type theory? Or more precisely, does the theory and the consistency proof, as described in Mario's thesis, apply "as is" also to Lean 4?

[Marcus Rossel]

AFAIK it's not exactly the same, as nested inductives have been pushed into the kernel to some extent in Lean 4 (I might be wrong about this though).

[Marcus Rossel]

So I'm guessing the inductive specifications in Mario's thesis are a bit less expressive than what Lean supports now.

[Sebastian Ullrich]

Yes, primitive mutual inductives, structure eta, and reduceBool/Nat are the big changes. I'm intending to write all of them down some time soon.

[Mario Carneiro]

Structure eta should be relatively easy to add to the theory; it was actually already using some aspects of structure eta to make the reduction to W types work. Primitive mutual/nested inductives should not be fundamentally harder, the tricky bit is getting the exact rules that the kernel uses. reduceBool/Nat is kind of hopeless, we can't prove anything about consistency in the presence of it

[Mario Carneiro]

actually that's not quite true, we just have to assume all the reduceBool applications are consistent with the model's notion of equality

[Mario Carneiro]

still it's not as self-contained of a claim as one would like

[Gabriel Ebner]

IIRC, reduceBool was never intended to be used for formalized mathematics anyhow. It's perfectly reasonable to exclude it from the theory, i.e., treat it the same as sorry.

[Ulrik Buchholtz]

Hm, here is says (about reduceBool): “This feature is useful for performing proofs by reflection.”
Is this not still the plan?

[Mario Carneiro]

I think it depends on how much trust you are willing to give the overall system

[Mario Carneiro]

some applications have more "trust budget" than others

[Mario Carneiro]

For anything where we want to be able to prove a big theorem and then look at #print axioms and be convinced that it worked, or anything where we want the proof to be exportable to external verifiers, I think reduceBool is not suitable

[Mario Carneiro]

For big proofs where significant computation or verification of programs is part of the task (like the original Appel & Haken proof of 4-color theorem), I think reduceBool is a good way to incorporate the result in a formal system and prove what can be proved while trusting the computer for the part that would be otherwise infeasible

[Mario Carneiro]

I think there are also some low hanging fruits in making reduceBool more auditable, for example gathering a list of all implementedBy functions that are transitively reachable by the inputs to reduceBool

[Kevin Buzzard]

The mathematical community nowadays are in general completely accepting of unverified computational proofs if the problem is clearly far too big to be done by hand. For example the proof of ternary Goldbach is "here's hundreds of pages of hard maths dealing with N>10^30 and if anyone found a mistake then this would be regarded as a catastrophe until it was fixed, and for N<10^30 we wrote some bespoke code (which relied on another verification of binary Goldbach for N<10^18 which we just assumed) and we ran it once and maybe nobody else looked at it, and it printed "yes" at the end"

[Kevin Buzzard]

Sounds to me like reduceBool (and GMP) is acceptable for one half of the proof but not the other

[Ulrik Buchholtz]

Thanks. It's an interesting choice to limit reflection to “large-scale reflection” (contra ssreflect!). And even if the trust is slightly smaller for results proved using reduceBool than not, it should still be many orders of magnitude better than for something done with C-code hacked together by mathematicians and which only ran once.

[Kevin Buzzard]

And slower ;-)

[Reid Barton]

It won't be much slower though, that's the point--maybe the name is a bit misleading in that it it suggests #reduce, but reduction is exactly what it avoids.

[Leonardo de Moura]

As @Gabriel Ebner pointed out above, reduceBool was never intended to be used for formalized mathematics. We added this feature for users that do not mind large trusted code bases which contain many bugs. For example, many software verification tools trust complex SMT solvers like CVC5 and Z3. reduceBool dramatically increases the size of the trusted code base. The Lean compiler is a complex piece of software, and contains many bugs and corner cases that can be exploited to prove False. @Kevin Buzzard reduceBool is way more dramatic and using GMP in the kernel. GMP is heavily tested, implements a clear specification/functionality, and can be replaced with many other (heavily tested) packages that implement the same functionality. In the future, it is even feasible to replace it with a verified version. On the other hand, reduceBool relies on the Lean compiler, a new piece of software implementing a much more complex specification/functionality. We have only one Lean compiler at this point, and it is infeasible to verify it right now.
I deeply regret adding the reduceBool feature, the intended user never used it, and it generates a lot of confusion, and recurrent theads. I thought the warning at reduceBool would make it clear this is a unsafe feature. I will try to make it clear how dangerous this feature is, and will add the following example to the documentation https://github.com/leanprover/lean4/blob/master/tests/lean/run/nativeReflBackdoor.lean
@Mario Carneiro Making reduceBool more auditable is a good thing, but it is not enough. I am assuming you are trying to address this issue https://github.com/leanprover/lean4/blob/master/src/Init/Core.lean#L1050-L1052, this is good, but we would still be trusting the Lean compiler, a complex piece of software.
Finally, recall that any development using reduceBool will be much harder to check using an external type checker. Malicious users may exploit bugs in the Lean compiler, and inject invalid proofs in big descentralized and cooperative projects like Mathlib.

[Mac]

Leonardo de Moura said:

I deeply regret adding the reduceBool feature, the intended user never used it, and it generates a lot of confusion, and recurrent theads. I thought the warning at reduceBool would make it clear this is a unsafe feature.

I would like to make a brief comment in defense of reduceBool/nativeDecide. While not useful (and often counterproductive) for mathematics, it is quite nice for software verification -- especially for quick and dirty proofs about small snippets of code. It allows one to write proofs of functionality for algorithms that would otherwise be very difficult to reason about in Lean, including those using partial and extern functions (e.g., String utilities, FFI code). I think that when Lean moves past the mathport phase into the more general programming phase there is hope that reduceBool may move from being often a liability to a significant benefit.

[Mario Carneiro]

@Leonardo de Moura It's true that the lean compiler is large and complex, but for some reason or another most folks have a blind spot for compiler correctness, and worrying about / defending against bugs in the compiler itself is on the paranoid end of the spectrum. But perhaps more to the point, once you take away the extension points the compiler is at least a bounded thing that you can audit without regard to the thing being compiled. But the extension points make this kind of auditing insufficient, and implementedBy has all the ease of use and power of an added axiom, as your test case evidences.

Besides implementedBy and extern, what other extension points are there in the compiler? The only one that comes to mind is csimp. This one at least uses provable equalities, but an auditing tool would still need to track down uses of csimp lemmas in called functions to find out which axioms were involved in the proofs of these equalities as well (since you could use implementedBy to redirect the compiler to a different definition which is csimp'd by sorry and you could lose track of the sorry dependence if you aren't careful).

I agree with Mac that reduceBool is not a mistake: it definitely has use cases, and I think we should encourage a more graded notion of trust in formal methods more generally, as long as we are upfront about what we are trusting. I think this discussion has helped to answer the question of what mathlib4 should do with regard to use of reduceBool: it should be banned in most of the library, except possibly for a clearly marked subfolder for theorems that require this dependency.

[Leonardo de Moura]

@Mario Carneiro

for some reason or another most folks have a blind spot for compiler correctness, and worrying about / defending against bugs in the compiler itself is on the paranoid end of the spectrum.

I agree with the statement only for compilers that are heavily used and tested like gcc, clang, ghc. This is not the case for the Lean compiler. Even these heavily tested compilers have many corner-case bugs that can be exploited by adversarial users.

But perhaps more to the point, once you take away the extension points the compiler is at least a bounded thing that you can audit without regard to the thing being compiled.

Who is going to do the audit? It is a lot of work, there is also the runtime that contains low-level C code.

Another issue is that we lose the capability of checking Lean developments with external type checkers. The external type checkers would have to implement an efficient reduceBool which is a lot of work. I don't want to give up that.

Note that by the same token, one could "audit" and then trust SMT solvers, but I think this is a recipe for getting a bunch of proofs of False.

I agree with Mac that reduceBool is not a mistake: it definitely has use cases, and I think we should encourage a more graded notion of trust in formal methods more generally

This is really subtle, and it is hard to communicate to users how much they are sacrificing when they use reduceBool.
I think Lean has a really good track record for soundness, and the last thing I want is to jeopardize that. Imagine the following "disaster scenario", a really important result is proved in Lean, but it is due to a bug in the runtime or compiler.

I think this discussion has helped to answer the question of what mathlib4 should do with regard to use of reduceBool: it should be banned in most of the library, except possibly for a clearly marked subfolder for theorems that require this dependency.

Yes, I think it should be banned from Mathlib 4. It is fine for exploratory work, quick experiments, and software verification projects where none of the members are adversarial.

That being said, I think we all want a better story for "proof by reflection." We will work on that in the future. We can implement a much simpler compiler for this use case, and make sure it is feasible to verify it.

Besides implementedBy and extern, what other extension points are there in the compiler?

This is a low priority right now, but we will add support for tracking this kind of dependency (csimp included).