Well, how do we know there aren't errors in their construction within the lean code? Does it just "not compile" or something, or is it deeper / more fundemental than that.

https://ammkrn.github.io/type_checking_in_lean4/trust/trust....