3 ms·

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

by aizk 23d 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.

Jblx2 23d ago
https://ammkrn.github.io/type_checking_in_lean4/trust/trust.html https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
frotaur 23d ago
that's essentially it, if the proof is incorrect it does not compile which signifies a problem in some step.