この記事は後半です。前半は Qiita にあります: AIの反証が通った日、Leanは番人を増やした
画像: github.com より
前半では、AI 支援のコラッツ反証が「数学の発見」ではなく、Lean カーネルの不具合を踏んだ可能性がある、という流れを見た。そこで開発者は、公式カーネルだけに頼るのをやめ、外部チェッカーを複数並べる方向へ舵を切った。ここで大事なのは、verified kernels が「Lean 全体の完全な正しさ」を証明するわけではないことだ。証明しているのは、受理した環境に対して False の証明が混じらないこと、そしてその受理条件がきちんとモデルに落ちることだ。
con-leche の proof idea は、その点をかなり率直に示している。checkDecls が .ok env を返したなら、env には集合論的なモデルが存在する。False は空集合、Eq は集合の等号として解釈されるので、False を導くような環境はモデルを持てない。つまり、カーネルの「受理」と意味論の「真理」をつなぐ橋を、Lean の内部の型理論だけでなく、外側のモデルで確保している。
ただし、この橋は万能ではない。con-leche の証明は、少なくとも開発者自身がそう書いているように、実際のドライバ全体を覆っていない。入力を読むところ、スレッドを立てるところ、進捗を出すところは別物だ。証明が守るのは、その先にある checkDecls の核だ。
今回の事後報告で刺さるのは、バグの入り口がかなり狭いことだ。問題の #14576 は、ネストした帰納型の扱いで、あるパラメータが補助型生成の段階で消えてしまう点にあった。しかも到達可能なのはメタプログラミング経由だけで、普通のフロントエンドは型検査で止める。つまり、日常的な Lean の使い方では気づきにくいが、カーネルに直接食わせると危ない、というタイプの不具合だった。
ここで外部チェッカーが効く。とはいえ、最初に見つかったのは別のチェッカー nanoda も別箇所の不具合を持っていた、という事実だった。Lean 本体の bug と nanoda の bug は別物で、たまたま同じ証明が両方の穴を通った。だから「独立実装だから安心」とは言い切れない。実際、開発者ブログでは lake check --paranoid で複数のカーネルをまとめて走らせる方針が示されている。公式カーネルに加えて、nanoda、lean4lean、con-leche、con-ron を並べ、さらに公式カーネルの hardened 版も見る。見逃しを一つの実装に押しつけない、という設計だ。
この運用の意味は単純ではない。1 個の番人が倒れないことを祈るのではなく、番人同士を照合して、差分が出たら止める。そのために lake check は sandbox 内で走る。もし検査器自身に危ない入力を与えられても、被害を閉じ込める意図がある。
con-leche の設計で印象的なのは、Lean の Expr に依存しない独自の項表現を持っている点だ。これで未検証の C++ ルーチンを避ける。帰納型の扱いも、mutual と nested を一様な方針で処理する。公式カーネルの nested-to-mutual 変換に寄せすぎないので、今回のような実装のひずみを別の見方で捉えられる。
一方で、con-leche は「実装が Lean で書かれている」以上の弱点も認めている。ビルドされたコンパイラや runtime にバグがあれば、そこは残る。だから con-ron が必要になる。con-ron は con-leche を Rust に写したもので、Lean 上の証明に対して Rust 実装が追随することを示す。開発者ブログでは、これで Lean の compiler や runtime、bignum ライブラリに潜む不具合が同時に Rust 側にも居る可能性は低いので、両方で通すとかなり強い保護になると説明されている。
ここでの肝は、Rust 版が単なる再実装ではないことだ。Aeneas を使って Rust コードが Lean 側の checking algorithm を refine することを証明している。つまり、「似ている」ではなく「この範囲では対応している」を形式化している。
自分なら、普段は lake check の標準実行で十分な速度と開発体験を取り、CI では --paranoid を必須にする。理由は、外部カーネルの価値が高いのは、ふだん見えない穴を別の実装で炙り出すことだからだ。ローカルで毎回すべてを回すより、まずは既存の開発速度を落とさない形で差分検査をかける方が現実的だろう。
ただし、verified kernels があっても安心し切るのは早い。開発者自身が今後の課題として挙げているように、Mathlib 級、あるいはそれを超える巨大な開発では、今の外部カーネル連携はそのままでは持たない。バイナリ形式のエクスポートや増分チェックが必要になる。ここは「正しさの証明」だけでは埋まらない、運用の問題だ。
Lean は今、証明を受け入れる側の信頼を、単独のカーネルではなく複数の独立実装と形式証明で支えようとしている。コラッツの一件は、その必要性を劇的な形で可視化した。見えてしまった反証が本物かどうかは、最後には番人の側が決める。その番人自身を、今は Lean が Lean で証明している。
