Lean 증명 도구가 여러 검사기로 결과를 다시 확인하는 기능을 추가했다(leodemoura.github.io)

- Lean은 수학 증명과 프로그램의 정확성을 기계가 검사하는 증명 도구다. 이 글에 따르면 Lean v4.35.0에 lake check 명령이 들어가, 작업물을 내보낸 뒤 공식 검사기 leanchecker로 다시 검사할 수 있다. 전 과정은 기본적으로 샌드박스 안에서 실행된다. - lake check --paranoid 옵션을 쓰면 nanoda, lean4lean, con-leche, con-ron 네 개의 추가 검사기로도 같은 작업을 다시 확인한다. 공식 검사기의 메모리 강화 버전도 함께 돌아가, 메모리 오류가 조용한 오답 대신 검사 중단으로 드러나게 한다. - con-leche는 Lean으로 작성되고 일관성이 증명된 첫 커널이라고 원문은 밝힌다. 증명은 집합론 모델을 근거로 하며, 구현 실수 유형의 버그를 줄이는 접근이라고 설명한다. 전체 Mathlib 내보내기에서 공식 커널 대비 명령어 수 0.69배, 8개 스레드로 약 100초라는 수치는 저자가 밝힌 측정 결과다. - con-ron은 con-leche를 AI로 Rust에 옮긴 뒤 Aeneas 도구로 원래 검사 알고리즘과 일치함을 증명한 커널이다. Aeneas는 Lean으로 Rust 코드를 검증하는 도구다. 두 커널을 함께 쓰면 Lean 컴파일러나 런타임 쪽 오류에 대한 보호가 높아진다는 것이 원문의 설명이다.