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のコンパイラやランタイム側のエラーに対する保護が高まるという。