Lean4Less discussion thread

Stream: general

[Rish Vaishnav]

Discussion thread for the Lean4Less announcement

[Violeta Hernández]

Interesting! Is def-eq proof irrelevance the only axiom within scope, or are there plans to expand this project to e.g. proving things without choice or LEM?

[Rish Vaishnav]

It's limited to eliminating definitional equalities, that is, equalities that are checked by the kernel and do not normally require proof. And in the process, it introduces axioms, like the prfIrrel axiom above (which is definitionally true in Lean). It builds the proof in parallel to normal kernel typechecking, and it doesn't do anything more intelligent, like trying to get around using proof irrelevance when it doesn't have to use it. So it's not applicable to translating proofs to evade the use of certain things like the axiom of choice or the excluded middle property. I do have plans to soon extend it to eliminate other defeqs, like struct and function eta for example (there's just a little bit more I need to parameterize first in order to try that out)

[Rish Vaishnav]

I should probably mention that I called the translation "Lean4Less" in the sense of "Lean for a smaller kernel", it's not at all a translation that tries to reduce the size of Lean terms, the translated terms will only get bigger (much bigger, in some cases)