Comment by aizk
17 hours ago
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.
17 hours ago
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....
that's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.