A formalization of Borel determinacy in Lean

この論文は、Lean 4 定理証明器を用いて、Martin の「Borel 決定性の純粋帰納的証明」に倣い、Gale-Stewart ゲームの定義と Borel ゲームの決定性に関する Martin の定理の証明を形式化したものである。

要約

数学の「無限ゲーム」を証明する：コンピュータに教えた驚きの物語

この論文は、**「無限に続く二人のゲーム」**において、必ずどちらかが勝つ戦略を持っているという、数学の難問をコンピュータに証明させたという画期的な成果について書かれています。

少し難しい数学用語を、日常の風景やゲームに例えて、わかりやすく解説しましょう。

1. 舞台は「無限の迷路」

まず、この話の舞台は「ガール・スチュアートゲーム」と呼ばれるものです。
想像してみてください。二人のプレイヤー（0 番と 1 番）が、無限に続く迷路を歩いています。

• 二人は交互に、迷路の分かれ道で「左」か「右」を選びます。
• この選択は永遠に続きます。
• 最後には、二人が選んだ道が一本の「無限に長い道（経路）」になります。
• その道が「赤い道」なら 0 番の勝ち、「青い道」なら 1 番の勝ち、というルールが決まっています。

このゲームの面白いところは、**「どちらかが必ず勝つ戦略を持っている」**という事実（決定性）が、ある条件（ボレル集合と呼ばれる複雑さのレベル）を満たす迷路であれば、証明できるということです。

2. 難問：なぜコンピュータはこれを嫌うのか？

この「無限の迷路」の証明は、数学者マーティンが 1975 年に発見しましたが、その証明は非常に複雑で、直感的ではありません。

• 通常の証明: 「無限の迷路」を、小さな「有限の迷路」の積み重ねとして考え、それを一つずつ解決していく方法です。
• コンピュータの壁: 従来の数学の証明では、「もしこの道が存在しない場合は、適当なダミーの値（ゴミのような値）を入れておこう」という手抜きが許されていました。しかし、厳密な論理を扱うコンピュータ（Lean というツール）にとって、この「手抜き」は致命的なエラーになります。「存在しない道」に「ゴミ」を放り込むと、計算が破綻してしまうのです。

著者のスヴェン・マンテさんは、**「ゴミを使わず、本当に存在する道だけを厳密に扱う」**という、人間が普段やっているような自然な数学の定義を、コンピュータにそのまま受け入れさせようとしました。

3. 解決策：「包み紙」の魔法

この難題を解決するために、著者は 2 つの工夫をしました。

① 「包み紙」で問題を隠す（カテゴリー論の活用）

証明の核心部分では、複雑な迷路を「より単純な迷路」に置き換える作業が必要です。
これを、**「複雑な迷路を、透明な包み紙で包んで、外側から単純な迷路に見せる」**ようなイメージで扱いました。

• 数学的には「逆極限（インバース・リミット）」という難しい概念を使いますが、要は「無限に続く迷路の構造を、レベルごとに整理して、一つずつつなげていく」作業です。
• 著者は、これを「箱詰め」のように整理し、コンピュータが混乱しないように、数学の「箱（カテゴリー）」という枠組みを使って証明しました。

② 「ゴミ」を使わない勇気

著者は、数学の定義を「存在するものだけ」で厳密に記述しました。

• 従来の方法（ゴミあり）: 「道がない場合、0 番の勝敗は『0』とする（実際は 0 番はそこにはいないのに）」
• 著者の方法（ゴミなし）: 「道がない場合は、その議論自体が成立しない（エラー）」
• これにより、証明は人間が紙に書くのと同じくらい自然になりました。ただし、コンピュータにとっては、この「自然さ」が処理を重くする原因にもなりました。

4. コンピュータの「重り」問題と解決

「ゴミ」を使わないと、証明の過程で「この道は本当に存在するか？」というチェックが何度も繰り返され、計算が爆発的に遅くなるという問題が起きました。

• 例え話: 料理をするとき、毎回「この野菜は本当に新鮮か？」と確認するために、野菜を一度全部箱から出して、また箱に戻す作業を繰り返すようなものです。
• 解決策: 著者は、コンピュータに「この野菜は箱に入れたまま、中身は信頼していいよ」という**「メモ（補助定理）」**を自動的に作らせるプログラム（メタプログラム）を書きました。これにより、無駄な確認作業を省き、証明を完了させることができました。

5. なぜこれが重要なのか？

この研究は、単に「無限ゲーム」を証明しただけではありません。

• 数学と AI の架け橋: 非常に高度で抽象的な数学の証明を、コンピュータが厳密に検証できる形に変換することに成功しました。
• 新しい基準: 「ゴミ（ダミー値）」を使わずに、数学の定義をそのままコンピュータに教えることが可能であることを示し、今後の数学の形式化（コンピュータによる証明）の新しい道筋を作りました。

まとめ

この論文は、**「人間が直感的に行っている数学の『手抜き』や『省略』を、コンピュータに理解させるために、いかに工夫して『厳密な言葉』に翻訳したか」**という、技術と知恵の物語です。

著者は、複雑な無限の迷路を、コンピュータが迷子にならないように、一つ一つのステップを丁寧に整理し、最終的に「どちらかが必ず勝つ」という真理を、機械の論理で証明し抜きました。これは、数学の深淵をコンピュータの光で照らした、素晴らしい冒険でした。

技術概要

論文「A formalization of Borel determinacy in Lean」の技術的概要

本論文は、スヴェン・マンテ（Sven Manthe）によって執筆され、Lean 4 定理証明支援系を用いて「ボレル決定性（Borel determinacy）」を形式化した研究報告です。以下に、問題設定、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題設定と背景

• 決定性（Determinacy）: 無限の二人零和ゲーム（ゲイル・スチュワートゲーム）において、どちらかのプレイヤーが勝つための戦略（勝つ戦略）を持つことを「決定性」と呼びます。
• ボレル決定性: 1975 年にマーティン（Martin）によって証明された定理で、ボレル集合を報酬集合とするゲームは決定性を持つという主張です。これは ZFC（選択公理付きのツェルメロ・フレンケル集合論）内で証明可能ですが、証明には非常に強力な部分集合論（通常の定理よりもはるかに大きな ZFC の断片）が必要とされています。
• 形式化の課題: これまで決定性の形式化は閉集合（closed sets）に限定されており、ボレル集合を含むより一般的なクラスでの形式化は証明支援系で行われていませんでした。また、Lean の数学ライブラリ（mathlib）の既存の慣習（部分関数を「ジャンク値」で扱う方法）と、数学的な直観（定義域を制限する依存型）の間のギャップをどう埋めるかという設計上の課題もありました。

2. 手法と形式化のアプローチ

本論文は、マーティンの「純粋帰納的証明（A purely inductive proof of Borel determinacy）」[Mar85] に基づき、いくつかの重要な適応と改良を加えて Lean 4 で形式化を行いました。

2.1 証明の骨子

証明は、ボレル集合の構成に対する帰納法ではなく、より強い性質である**「解きほぐし可能性（unravelability）」**の帰納法に基づいています。

1. 閉ゲームの解きほぐし: 閉集合を報酬とするゲームが「解きほぐし可能」であることを示します。
2. 普遍解きほぐし可能性（Universal Unravelability）: 通常の「解きほぐし可能性」ではなく、任意の被覆（covering）に対して解きほぐし可能であるという「普遍解きほぐし可能性」を導入しました。これにより、可算和の扱いにおいて、マーティンの証明で用いられた超限帰納法を避け、ボレル集合の構成に対する直接帰納法が可能になります。
3. 逆極限の構成: 可算和の扱いには、ゲームの逆極限（inverse limit）の構成が必要です。ここで、マーティンの証明における「レベルごとの同一視」という扱いにくい部分を、圏論的な補題（逆極限の性質）を用いて厳密に処理しました。

2.2 Lean における実装上の技術的選択

• 戦略の表現: 関数としての戦略（functional strategies）と、戦略木（strategy trees）の両方を定義しましたが、実装の多くは関数としての戦略（PreStrategy）に基づいています。これは、特定の戦略を定義する際に関数の方が再帰を避けやすく、扱いやすいためです。
• 部分関数の扱い（依存型 vs ジャンク値）:
  • mathlib の慣習: 部分関数を全関数 $X \to Y \sqcup \{\bot\}$ として定義し、定義域外では「ジャンク値（$\bot$）」を返す方法。
  • 本論文のアプローチ: 依存型を用い、定義域の条件（命題）を引数として関数に含める方法（$\{x \in X \mid P(x)\} \to Y$）。
  • 理由: 依存型のアプローチは、式を書き換える際に定義域の条件が自動的に維持されるため、証明の複雑さを減らし、直観的な数学的定義に忠実です。
• 自動化（Tactic）:
  • プレイヤーのターンを判定する長さの条件（偶数・奇数）を処理するために、リストの長さの展開と Presburger 算術ソルバー（omega）を結合した独自の tactic を開発しました。
  • 「$f$ が $k$-fixing である」という仮定を自動的に推論するために、型クラス推論（typeclass inference）を活用し、最大限の $k$ を「out-parameter」として扱う仕組みを実装しました。

3. 主要な貢献

1. ボレル決定性の初の実装: 証明支援系において、閉集合を超えたクラス（ボレル集合）の決定性が形式化されたのは初めてです。コード量は約 5,000 行で、その大半がマーティンの証明自体の形式化に充てられています。
2. 「普遍解きほぐし可能性」の導入: 可算和の扱いを容易にするため、マーティンの証明を改良し、超限帰納法を回避する「普遍解きほぐし可能性」の概念を定式化・証明しました。
3. 圏論的アプローチの活用: 可算和に対応する逆極限の構成において、マーティンの証明の「レベルごとの同一視」という非形式的な部分を、圏論（逆極限の性質）を用いて厳密に形式化しました。
4. 依存型を用いた部分関数の形式化: Lean/mathlib の既存の慣習（ジャンク値）に依存せず、数学的な定義に近い依存型ベースの部分を採用し、その利点と課題（パフォーマンス問題など）を具体的に示しました。

4. 結果と知見

• 証明の成功: Lean 4 および mathlib 上で、ボレル決定性の定理が完全に証明されました。
• パフォーマンス課題の解決: 依存型を多用するアプローチでは、証明項（proof terms）のネストが深くなり、計算時間が指数関数的に増加する問題が発生しました。これを解決するため、証明項を即座に補題として抽象化するメタプログラム（abstract、後に as_aux_lemma）を開発・実装し、実行時間を現実的な範囲に抑えました。
• 圏論ライブラリの利用: 木（tree）の圏 $\mathcal{C}$ がすべての極限を持つこと、およびレベル制限関手が極限を保存することを証明し、逆極限の構成を厳密に行いました。

5. 意義と将来展望

• 記述集合論の形式化の進展: ボレル決定性の形式化は、記述集合論のより高度な結果（解析的決定性など）や、大基数公理との関係を形式化するための基盤となります。
• 証明支援系の設計への示唆: 本論文は、部分関数の扱いにおいて「ジャンク値」ではなく「定義域の制限（依存型）」を採用することの妥当性を示しました。これは、数学的な直観をより忠実に反映でき、証明の簡潔さにつながる可能性があります。
• Lean の機能向上: 依存型を用いた形式化におけるパフォーマンス問題（証明項の展開による遅延）は、Lean 自体の機能改善（証明項の早期抽象化など）の必要性を浮き彫りにしました。

結論として、本論文は、強力な集合論的定理を現代の定理証明支援系で形式化する際の技術的課題（圏論的構成、依存型の実装、パフォーマンス最適化）を克服し、記述集合論の形式化における重要なマイルストーンを達成したものです。