3 ms·
You don't have to trust the full Lean toolchain, only the trusted proof kernel (which is small enough to be understood by a human) and any desugarings involved
by zozbot234 11mo ago
You don't have to trust the full Lean toolchain, only the trusted proof kernel (which is small enough to be understood by a human) and any desugarings involved in converting the theorem statement from high-level Lean to whatever the proof kernel accepts (these should also be simple enough). The proof itself can be checked automatically.
- tuhgdetzhh 11mo agoLets assume the kenerl is correct and a mathematian trusts it, now what happens if it is the proof itself that he cannot understand anymore because it has gotten too sophisticated? I think that this would indeed be a difference, and a crossing point in history of mathematical proofs.
- zozbot234 11mo agoIn principle, it's no different than failing to understand the details of any calculation. If the calculating process is executed correctly, you can still trust the outcome.