Lean теперь поставляется с проверенными ядрами

Lean Now Ships with Verified Kernels

Lean v4.35.0 включает команду lake check, которая перепроверяет разработки с помощью официального ядра leanchecker в песочнице. Также добавлены четыре альтернативных ядра: nanoda, lean4lean, con-leche и con-ron. Режим --paranoid запускает все ядра, включая вариант с защищённым аллокатором памяти. con-leche — первое ядро для Lean, написанное на самом Lean и доказанно непротиворечивое; его реализовал Claude под наблюдением Joachim Breitner. con-ron — трансляция con-leche на Rust с доказательством уточнения через Aeneas.