- Lean es una herramienta de pruebas que usa una máquina para comprobar la corrección de demostraciones matemáticas y de programas. Según este artículo, el comando lake check se ha añadido a Lean v4.35.0, por lo que puedes exportar tu trabajo y volver a comprobarlo con el verificador oficial leanchecker. Todo el proceso se ejecuta por defecto dentro de un entorno aislado (sandbox).
- Con la opción lake check --paranoid, el mismo trabajo se vuelve a comprobar con cuatro verificadores adicionales: nanoda, lean4lean, con-leche y con-ron. También se ejecuta una versión reforzada en memoria del verificador oficial, de modo que los errores de memoria aparecen como una detención de la comprobación en lugar de un resultado incorrecto silencioso.
- El artículo dice que con-leche es el primer núcleo escrito en Lean y demostrado consistente. La prueba se apoya en un modelo de teoría de conjuntos, y el enfoque se describe como una forma de reducir errores de tipo fallo de implementación. En la exportación completa de Mathlib, el autor informa una medición de 0.69 veces el número de instrucciones del núcleo oficial, usando 8 hilos en unos 100 segundos.
- con-ron es un núcleo que una IA portó de con-leche a Rust y que luego se demostró que coincide con el algoritmo de comprobación original mediante la herramienta Aeneas. Aeneas es una herramienta que verifica código Rust con Lean. El artículo explica que usar ambos núcleos juntos ofrece más protección frente a errores del compilador o del entorno de ejecución de Lean.
O: Resulta útil para investigadores que escriben pruebas en Lean y quieren ejecutar lake check --paranoid en su propio proyecto para comprobar que los resultados de los cuatro verificadores adicionales coinciden con los del verificador oficial.
X: Las cifras de 0.69 veces el número de comandos y de 100 segundos de con-leche son mediciones de los autores, y como las condiciones de medición no se han revelado por completo, conviene comprobarlas en su propio entorno.