5 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

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