alt Hacker NewsWell, 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.
Replies
frotaur • today at 8:27 AM
that's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.
https://ammkrn.github.io/type_checking_in_lean4/trust/trust....