But let's assume Lean is perfect:
- you have to trust your file system
- you have to trust your OS
- are you sure your monitor displays "proof is valid" correctly
- maybe there's a bug in your CPU hardware?
- or background radiation flipped a bit in your RAM
- do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".
But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".