ZFLean: a framework for set-level mathematics in Lean

以下は、Vincent Trélat による論文「ZFLean: a framework for set-level mathematics in Lean」の詳細な技術的サマリーです。

1. 問題提起

Lean などの証明支援系における現代の形式化は、主に数学的対象が構成された型である型理論（特に依存型理論）に基づいています。これは強力なアプローチですが、多くの場合で好まれる集合レベルの数学（ZFC）にとっては煩雑になり得ます。その理由は以下の通りです：

• 拡張的推論：構成ではなく要素に基づいた等号に関する推論。
• 部分性：Option 型や依存型で符号化するのではなく、関係を通じて自然に部分関数を扱うこと。
• 圏論的な推論：厳密な定義的等号ではなく、「同型まで」を考慮して作業すること。

課題： typed アシスタント（Lean の Mathlib の ZFC モデルなど）内の集合論的モデルで直接作業することは、以下のような大きな摩擦をもたらします：

• ボイラープレート：ユーザーは常に「側条件」（例えば、関係が well-defined であることを証明する、関数が全関数であることを証明する）を手動で管理しなければならない。
• 脆弱性：集合論的対象（ZFSet）とネイティブな Lean 型（Type）の境界を越える作業は手動であり、エラーを起こしやすい。
• 自動化の欠如：既存のツールは、集合論的証明を型付き証明と同様に流暢にするために必要な、特定の書き換えヒントや戦術（tactics）を欠いていることが多い。

2. 手法

著者は、Mathlib の既存の ZFC モデルを基盤とした Lean 4 ライブラリZFLeanを提示します。この手法は、集合レベルの開発を人間工学に基づいたものにするための均一な関係計算と相互運用性の橋渡しの作成に焦点を当てています。

中核的な設計選択：

• 基盤：集合を帰納的「前集合」（PSet）の拡張的商として構築する Mathlib の ZFC 実装を活用します。
• 関係計算：標準的な型理論のように関数を第一級全対象として扱うのではなく、ZFLean は関数を機能的関係として扱います。二項関係、部分関数、全関数に対する計算論を導入します。
• 戦術による自動化：このフレームワークは、well-formedness の側条件（例えば、合成が関係または関数であることを証明すること）を自動的に処理するように設計された、3 つの軽量戦術（zrel、zpfun、zfun）を導入します。
• 橋渡し：このライブラリは、標準的な ZFC 対象（例：ZFBool、ZFNat）と Lean のネイティブ型（Bool、Nat）の間に明示的な同型（橋渡し）を構築し、両世界間で性質を輸送可能にします。

3. 主要な貢献

A. 関係計算と自動化

• 定義：関係に対する逆、恒等、合成、定義域、値域、および像を形式化します。
• 関数性：部分関数（IsPFunc）と全関数（IsFunc）を区別します。
• 戦術：
  • zrel：集合が関係（$R \subseteq A \times B$）であることを証明する目標を処理します。
  • zpfun：集合が部分関数であることを証明する目標を処理します。
  • zfun：集合が全関数であることを証明する目標を処理します。
  • これらの戦術は、@[zfun] などの属性タグ付き補題を使用して側条件を再帰的に解決し、ユーザーからボイラープレートを隠蔽します。
• 記法：関数適用（@zf(x)）および $\lambda$-抽象化のための便利な構文を導入し、$\beta$-簡約、$\eta$-展開、および拡張性に関する定理を提供します。

B. 標準的構成

このライブラリは、普遍的特性を備えた、ZFC 内で定義された標準的な数学的対象のスイートを提供します：

• ブール値：代数的構造（論理積、論理和、否定）と場合分け消去子を持つ 2 要素集合 $B$。
• 自然数（$\mathbb{N}$）：最小の帰納的集合（フォン・ノイマン順序数）として定義されます。再帰子、帰納法原理、および算術演算を含みます。重要なのは、Lean の ring 戦術を活用するために CommSemiring 構造を備えている点です。
• 整数（$\mathbb{Z}$）と有理数（$\mathbb{Q}$）：自然数/整数の対の商型として構成され、演算は代表元から持ち上げられます。
• コ積とオプション：和型とオプション型の集合論的定義。

C. 同型と輸送

• 埋め込みと同型：単射関数と全単射関数を通じて、集合レベルの埋め込み（$A \hookrightarrow_z B$）と同型（$A \cong_z B$）を定義します。
• カントル・シュレーダー・ベルンシュタインの定理：フレームワーク内で形式化されています。
• 輸送：ZFC 構成が Lean のネイティブ型と同型であることを証明します（例：ZFBool $\simeq$ Bool）。これにより、ユーザーは豊富な Mathlib の型理論的ライブラリからの定理を、シームレスに集合論的文脈へ「輸送」できます。

D. ケーススタディ：カリー化同型

この論文は、カリー化同型：$C^{A \times B} \cong (C^B)^A$ を証明することで、フレームワークの実用性を示しています。

• 証明は、curryz と uncurryz を集合レベルの関数として定義します。
• フレームワークの自動化を用いて側条件（合成と像の well-definedness）を処理し、これらが相互逆関数であることを証明します。
• 証明スクリプトは標準的な数学的議論に密接に対応しており、自動化層が「退屈な」集合論的検証を処理します。

4. 結果

• アーティファクトの規模：このライブラリは、8,324 行の Lean コードと706 個の証明済み定理で構成されています。
• コンポーネントの内訳：
  • 関係計算：約 2,534 行（172 定理）。
  • 自然数：約 1,260 行（199 定理）。
  • 埋め込み/同型：約 1,626 行（31 定理）。
• 使いやすさ：ケーススタディは、このフレームワークが集合レベル形式化の摩擦を効果的に軽減することを示しています。ユーザーは、関係の合成が有効な関係であることを手動で証明することなく、標準的な集合論的議論に見える証明を書くことができます。
• 相互運用性：ZFSet とネイティブな Type の間を切り替える能力により、集合論的対象に対して Mathlib の代数的戦術（ring など）を再利用することが可能になります。

5. 意義

• 基盤の橋渡し：ZFLean は、単一の証明支援系内で「集合論的」と「型理論的」な数学の視点を効果的に調和させます。これにより、数学者は特定の課題に最も自然な基盤（拡張的集合対比構成的型）を選択しつつ、エコシステムの自動化へのアクセスを失うことなく作業できます。
• 人間工学：集合論に固有の退屈な側条件（所属証明、関係の well-definedness）を自動化することで、非専門家にとって Lean における ZFC 開発を実用的にし、大規模な形式化を可能にします。
• 拡張性：モジュール設計（関係計算＋標準的対象＋橋渡し）により、容易な拡張が可能です。今後の作業には、実数（コーシー列またはデデキント切断を介して）および基礎的な解析学の形式化が含まれます。
• 比較：Isabelle/ZF（ここで集合論は独立した対象論理である）や、型理論的自動化との深い統合が欠如していることが多い Rocq の集合論的開発とは異なり、ZFLean は証明を集合レベルに保ちつつ、Lean のネイティブな型理論的インフラを活用するハイブリッドアプローチを提供します。

結論として、ZFLean は Lean 4 内で ZFC における核心数学を行うための、堅牢で人間工学的に優れ、相互運用可能なフレームワークを提供します。これは、集合論的形式化への参入障壁を効果的に下げつつ、より広範な Mathlib エコシステムとの互換性を維持することに成功しています。