I am also not too impressed by the existence of second-party checkers in the context of a language that lacks decidable type checking. Because something has to give, these checkers will be (necessarily) incomplete in one way or another, most likely each in different ways. This is because lean’s failure of completeness of conversion almost certainly manifests in heuristic ways that are not predictable or replicable…

For a fail safe checker to provide confidence, it needs to be complete. This is not possible with Lean’s core language as designed, and it will not be possible for Lean itself until they find new leadership.

@ncf Two examples.

Soundly reducing a well-typed beta redex requires the domain which was used to type the abstraction's body to match the type of the argument, and the return type of the abstraction to match the type of the entire term. You get this for free only if Pi is injective, otherwise you need to do it by hand. The classic example is nat -> nat = nat -> bool which is a sound (definitional) equation (it's true in the cardinal model, for instance), which lets you type (fun x => 0) 0 : bool, but you need to prevent this from reducing by noticing that bool <> nat.

More frightening (and less known): congruence of application!! The issue here is more subtle, and depends of how exactly you set things up. But the idea is that the reasonable invariant for neutral comparison is to only assume that both sides are well-typed, but _not necessarily at the same type_ (assuming they have the same type cannot be preserved recursively, because eg knowing f u = f' u' have the same type does not tell you f and f' do). Your post-condition will then assert the neutrals are defeq at a given type. Now if you again think about comparing f u = f' u', you assume both applications are well-typed, thus also f and f' are, recursively compare them, learn they are defeq at some (x : A) -> B. Now you want to know you can compare u to u'. But these are normal forms, so now you must provide a type at which to do that comparison. Surely enough, A should do? Well now you have to establish u' : A knowing only f' u' is well-typed and f' : (x : A) -> B. Without some sort of Pi injectivity (+ maybe an argument on uniqueness of types which typically follows from it), you're toast.