Lean ahora incluye kernels verificados para blindar sus demostraciones

Lean Now Ships with Verified Kernels

Leonardo de Moura anuncia que Lean v4.35.0 incorpora el comando lake check, que reexporta un desarrollo y lo revalida en un sandbox con leanchecker. Además distribuye cuatro kernels externos —nanoda, lean4lean, con-leche y con-ron— que se ejecutan juntos con lake check --paranoid. con-leche, escrito en Lean y con prueba formal de consistencia, fue implementado por Claude bajo supervisión de Joachim Breitner; con-ron es su traducción a Rust verificada con Aeneas.