Lean prüft Beweise jetzt mit vier unabhängigen, teils formal verifizierten Kernels
Lean Now Ships with Verified Kernels
Leonardo de Moura kündigt an, dass Lean ab Version 4.35.0 mit dem Befehl `lake check` Entwicklungen in einer Sandbox gegen den offiziellen Kernel `leanchecker` prüft. Mit `--paranoid` werden zusätzlich die vier neuen Kernel nanoda, lean4lean, con-leche und con-ron ausgeführt. con-leche ist der erste in Lean geschriebene und formal als konsistent bewiesene Kernel; con-ron ist eine per Aeneas verifizierte Rust-Übersetzung. So sollen Implementierungsfehler im Kernel als Fehlerklasse ausgeschlossen werden.
Da con-leche einen formalen Konsistenzbeweis besitzt, liegen verbleibende Unsoundness-Fehler höchstwahrscheinlich im Compiler oder in der Laufzeitumgebung von Lean (einschließlich der Bignum-Bibliothek).