3 ms·
Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but
by munchler 2y ago
Lean has a small “kernel” that has been independently checked multiple times, and the rest of Lean depends on the kernel. A soundness bug is still possible, but pretty unlikely at this point.
https://lean-lang.org/lean4/doc/faq.html https://lean-lang.org/lean4/doc/faq.html
- norlygfyd 2y agoSoundness 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.