3 ms·
Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It i
by norlygfyd 2y ago
Soundness of Lean requires more than correctness of the kernel - it requires that the theory be sound. That, frankly, is a matter of mathematics folklore. "It is known" that the combination of rules Lean uses is sound... unless it isn't.
- munchler 2y agoThat would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.