Lean v4.35.0、検証済みカーネルを含む追加カーネル4種を同梱
Lean v4.35.0 には4つの追加カーネル（nanoda、lean4lean、con-leche、con-ron）が同梱された。そのうち con-leche は Lean で書かれた最初のカーネルで、無矛盾性が証明されている。
Lean v4.35.0 は lake check コマンドを備え、開発物を外部カーネルで再検査できるようになった。2026年10月15日時点の記事で、Lean 開発元の Lean FRO の関係者らが関わるプロジェクトの内容が紹介されている。
発表内容
lake check は開発物をエクスポートし、公式カーネルである leanchecker で再検査する。検査の全工程はサンドボックス内で実行され、lake check --inadvisably-no-sandbox で無効化できる。
lake check --paranoid を実行すると、4つのカーネルすべてで開発物を再検査できる。このオプションでは、強化されたメモリアロケータでビルドした公式カーネルの派生版も実行される。
con-leche の検証
con-leche は Claude（Fable and Opus）が実装し、Lean FRO の Joachim Breitner の強い監督のもとで無矛盾性が証明された。ここでの無矛盾性とは、con-leche が受理するすべての環境が集合論におけるモデルを持つことを指す。このモデルは Mario Carneiro による Lean の型理論のモデルに従っている。
証明自体は公式 Lean カーネルで検査され、モデルに用いた集合論の無矛盾性を前提としている。
全 Mathlib エクスポートにおいて、con-leche は公式カーネルの 0.69x の命令数を実行した。8スレッドを用いると、ライブラリ全体の検査に約100秒を要した。
Joachim は AI を使って con-leche を Rust に翻訳し、Aeneas を用いて Rust 版（con-ron）が con-leche の検査アルゴリズムを精緻化していることを証明した。
カーネル刷新と今後
Arthur Adjedj は、カーネル刷新計画（issue #14977）に取り組んでおり、これを実装する複数の PR を提出している。Joachim はこれらの PR をレビューし、con-leche の証明に修正を加えている。
記事では、Lean のライブラリ規模として以下の数値が挙げられている。
- Mathlib: 2.5M LoC
- Anthropic's FLT: 13M LoC
- Tau Ceti: 3M LoC（記事では「すでに3Mを超え、急速に増加している」とされる）
- The General Courtade–Kumar theorem repo: 50M LoC を超えるとされる
筆者の見立て
- 筆者は、con-leche を構築したコンパイラやランタイムにバグが存在する可能性があり、完全に堅牢ではないと解釈している。
- 筆者は、残存する健全性バグは Lean のコンパイラまたはランタイム（bignum ライブラリを含む）にある可能性が最も高いと予想している。
- 筆者は、同じバグが Rust のコンパイラやランタイムにも存在する可能性は非常に低いと予想している。
- 筆者は、con-leche と con-ron の両方で証明を検査することで、この種のバグに対して高い保護水準が得られることを示唆している。
- 筆者は、con-leche のアプローチが、カーネル実装におけるプログラミングミスという種類のバグを完全に排除すると解釈している。
- 筆者は、lean4lean の検証が今後数か月以内に完了し、検証済みカーネルが3つになると予想している。
- 筆者は、lean4lean の検証が重要であると論じている。その実装が公式の C++ カーネル実装に非常に忠実に従っているためである。
- 筆者は、外部カーネルを用いる現行の手法は、この規模の開発物には拡張できないと論じている。
- 筆者は、AI エージェントは Lean のソフトウェアの脆弱性を発見するのに非常に効果的であると論じている。
この記事は元記事の事実のみに基づいて自動生成されました。
出典
- 媒体名: Leonardo de Moura（ブログ）
- 元記事タイトル: Lean Now Ships with Verified Kernels — Leonardo de Moura
- URL: https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/