概要
マッチング理論・意思決定理論・オークション理論の主要定理を Lean 4 で形式化する。特にマッチング理論は、離散凸解析（Murota の M♮凹関数・粗代替性）の観点から証明を定式化する。Gale–Shapley、Kelso–Crawford、Fujishige–Tamura のように別々に語られてきた定理を「M♮凹関数の性質」という共通の土台に乗せて機械化すれば、その先にある未解決問題（完全代替性を超える取引ネットワークでの安定結果の存在、カップルつきマッチング等）に対して、仮定の境界を厳密に切り分ける道具ができる。
なぜ重要なのか（Why）
経済学の定理を定理証明器に載せる動きは、2025〜2026年に一気に加速した。2025年には vNM 期待効用定理（arXiv:2506.07066）と Simon の限定合理性（arXiv:2507.07052）が Lean 4 で機械証明された。2026年6月には、同名の2つの EconCSLib が EC'26 の AI-EconCS ワークショップで発表された。1つは Bei らによる4万行超・1,300定理超のライブラリで、Nash 均衡、Vickrey/VCG、Myerson の最適オークション、Arrow の定理、Gibbard–Satterthwaite、Gale–Shapley の受入保留方式までを Mathlib の上でカバーする（arXiv:2606.16144）。もう1つは Garg による「LLM が Lean を書き、Lean が検査し、人と LLM が意味を判定する」ワークフローで、Roth (1982) や Edelman–Ostrovsky–Schwarz (2007) の GSP オークションを含む20本の論文を丸ごと形式化した（arXiv:2606.13306）。それ以前にも Isabelle での VCG 組合せオークションの形式化（AFP, 2015）や Coq でのダブルオークションの検証（JAR 2025）はあり、「オークション理論は形式化できる」こと自体は既に示されている。
しかし、これらのどれも粗代替性（gross substitutes）や M♮凹性、離散凸解析には触れていない。Kelso–Crawford (1982)、Hatfield–Milgrom (2005)、Fujishige–Tamura (2007) の Lean 形式化は見当たらず、Mathlib には Matroid はあるが M凸集合・劣モジュラ関数・粗代替性の定義は存在しない。一方で離散凸解析の側では、Murota が2016年に J. Mechanism and Institution Design で「M♮凹性は粗代替性と同値であり、M-L 共役性・離散分離定理・離散不動点定理から均衡の存在と価格ベクトルの束構造が出る」という形で経済学・ゲーム理論への道具立てを整理し、Fujishige–Tamura は安定結婚問題と割当ゲームを M♮凹関数で統一している。Kojima–Tamura–Yokoo (JET 2018) は制約つきマッチングで病院側選好が M♮凹なら一般化 DA が医師側耐戦略的になることを示し、Murota–Shioura は2026年4月にも多需要モデルへの上昇オークション拡張を離散凸解析で与えている（arXiv:2604.27765）。つまり、経済学側の証明はすでに「離散凸解析の言葉」で書き直され続けているのに、形式化はまだ古典的な組合せ論の言葉に留まっている。
このギャップを埋める価値は2つある。1つは、証明を共通の抽象（M♮凹関数の性質）に乗せることで、個別定理の形式化を使い回せる部品にできること。もう1つは、未解決問題の周辺で「どの仮定を落とすと何が壊れるか」を機械的に検査できるようになることだ。取引ネットワークでは完全代替性が安定結果と競争均衡の存在を保証する極大領域であることが知られており（Hatfield–Kominers–Nichifor–Ostrovsky–Westkamp, JPE 2013）、カップルつきの研修医マッチングでは安定マッチングの存在判定が強い制限下でも NP 完全である（Biró–Manlove–McBride 2014）。粗代替性の側でも、Ostrovsky–Paes Leme のマトロイド基底評価予想が Tran (2019) により n≥4 で反証され、近似版は開いたままである（Paes Leme のサーベイ §11）。仮定と結論の対応を Lean で厳密に持つことは、これらの境界を探る作業の基盤になる。本人の言葉を借りれば「離散凸解析の観点から証明を定式化すると、未解決問題に応用が効きそうな気がする」というのが出発点である。
この研究の主な貢献・期待される成果（What）
- 離散凸解析の基礎（M凸集合、M♮凹関数、L♮凸関数、粗代替性との同値性）を Mathlib 互換の Lean 4 ライブラリとして定義・証明する。Mathlib の Matroid の上に載せ、既存の資産と接続する
- 既存の Lean 4 の Gale–Shapley 形式化（hwatheod/galeshapley-lean、EconCSLib）を起点に、Kelso–Crawford → Hatfield–Milgrom → Fujishige–Tamura の順で、安定結果の存在定理を M♮凹性から導く形で形式化する。最初の一歩は「Gale–Shapley の安定性証明を M♮凹関数の性質の系として再証明する」こと
- 意思決定理論（vNM の先の期待効用まわり）とオークション理論（Myerson の補題・収入同値定理・VCG）の主要定理を同じリポジトリに揃え、EconCSLib と重複しない範囲を明確にして相互参照する
- 形式化の副産物として、既存の手証明で暗黙だった仮定（有限性、選好の完備性、タイブレーク等）を列挙し、未解決問題（完全代替性を超える領域、カップルつきマッチング）に対して「反例が出る最小の仮定の落とし方」を機械的に探索できる環境を作る
- LLM による自動形式化（Garg 型のワークフロー）を離散凸解析の定義群に適用し、人が定義を設計し LLM が補題を埋める分業がこの分野で成り立つかを検証する
先行研究・関連ワーク
- EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research (arXiv:2606.16144) (Bei, Ma, Jing, Fu, Tang, EC'26 AI-EconCS): 4万行超・1,300定理超。Vickrey/VCG、Myerson 最適オークション、Arrow、Gibbard–Satterthwaite、Gale–Shapley DA、競争均衡、Brouwer/Scarf 不動点。→ 本研究が最も密に重なる既存資産。粗代替性・離散凸解析は未カバーで、そこが本研究の差分
- EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research (arXiv:2606.13306) (Garg, 2026): LLM が Lean を書き Lean が検査するワークフローで20本の論文を形式化（Gale–Shapley 1962、Roth 1982、EOS 2007 GSP 等）。→ 自動形式化の作業手順のリファレンス
- From Axioms to Algorithms: Mechanized Proofs of the vNM Utility Theorem (arXiv:2506.07066) (2025): 期待効用表現の存在と一意性を Lean 4 で証明。→ 意思決定理論パートの起点
- Quantifying Bounded Rationality: Formal Verification of Simon's Satisficing (arXiv:2507.07052) (2025): 限定合理性の Lean 4 形式化。→ 同上
- Discrete Convex Analysis: A Tool for Economics and Game Theory (arXiv:2212.03598) (Murota, J. Mech. Inst. Design 2016): M♮凹性⇔粗代替性、M-L 共役性、離散分離・不動点定理、反復オークション、安定結婚と割当ゲームの統一まで。→ 形式化すべき定義と定理の一覧表そのもの
- A Two-Sided Discrete-Concave Market with Possibly Bounded Side Payments (Fujishige–Tamura, MOR 2007): 安定結婚と割当ゲームを M♮凹関数で統一し、対安定結果の存在を示す。→ 本研究の中心的な形式化ターゲット
- Job Matching, Coalition Formation, and Gross Substitutes (Kelso–Crawford, Econometrica 1982): 粗代替性のもとでの均衡存在。→ 粗代替性の原典
- Matching with Contracts (Hatfield–Milgrom, AER 2005): 大学入試・Kelso–Crawford・パッケージオークションの統一と労働者側耐戦略性。→ 中間の形式化ターゲット
- Gross substitutability: An algorithmic survey (Paes Leme, GEB 2017): GS = M♮凹 = valuated matroid の同値関係と、§11 の未解決問題リスト。→ 「形式化が効きそうな未解決問題」の出所
- Designing Matching Mechanisms under Constraints: An Approach from Discrete Convex Analysis (Kojima–Tamura–Yokoo) (JET 2018): 病院側が M♮凹なら一般化 DA が耐戦略的。→ 離散凸性から耐戦略性を導く実例
- Extension of Excess Demand Ascending Auction to Multi-Demand Model by Discrete Convex Analysis Approach (arXiv:2604.27765) (Murota–Shioura, 2026): 均衡価格を L♮凸 Lyapunov 関数の最小点として捉える。→ この分野が現在も動いている証拠
- Stability and Competitive Equilibrium in Trading Networks (Hatfield et al., JPE 2013): 完全代替性が存在保証の極大領域。→ 未解決問題の境界の出所
- The Finite Matroid-Based Valuation Conjecture is False (arXiv:1905.02287) (Tran, 2019): Ostrovsky–Paes Leme 予想を n≥4 で反証。→ 反例探索を形式化で支援できる典型例
- hwatheod/galeshapley-lean: Lean 4 の Gale–Shapley 形式化。安定性・提案側最適・Dubins–Freedman・安定マッチングの完備束まで。→ 既存の Lean 資産として最初に接続する対象
- VCG - Combinatorial Vickrey-Clarke-Groves Auctions (Isabelle AFP, 2015) / Double Auctions: Formalization and Automated Checkers (arXiv:2410.18751) (Coq, JAR 2025): 他の証明器でのオークション形式化。→ 何が形式化済みで、Lean に移すべきものは何かの参考
Nyx の関連する取り組み・シナジー
対象となる読者・協力者
- Lean が書けて、マッチング理論・オークション理論・意思決定理論に興味がある人
- 離散数学（マトロイド、劣モジュラ、離散凸解析）に強い人
- 経済学者・メカニズムデザイン研究者で、自分の定理を機械証明にしたい人
- LLM による自動形式化（AI-EconCS 系）に取り組む人
想定される難易度・期間
- 難易度: 高（離散凸解析の基礎定義を Mathlib 互換で作るところから。Gale–Shapley 単体なら既存資産があるので入口は低い）
- 期間目安: 半年以上（Gale–Shapley の再証明までは1〜2ヶ月、Fujishige–Tamura までで半年、未解決問題への応用は1年超）
キーワード・タグ
Lean 4, mathlib, mechanism design, matching theory, discrete convex analysis, M♮-concave, gross substitutes, stable matching, auction theory, Myerson, VCG, decision theory, EconCSLib, autoformalization
その他の関連リンク
連絡先・ディスカッション
contact@nyx.foundation
概要
マッチング理論・意思決定理論・オークション理論の主要定理を Lean 4 で形式化する。特にマッチング理論は、離散凸解析（Murota の M♮凹関数・粗代替性）の観点から証明を定式化する。Gale–Shapley、Kelso–Crawford、Fujishige–Tamura のように別々に語られてきた定理を「M♮凹関数の性質」という共通の土台に乗せて機械化すれば、その先にある未解決問題（完全代替性を超える取引ネットワークでの安定結果の存在、カップルつきマッチング等）に対して、仮定の境界を厳密に切り分ける道具ができる。
なぜ重要なのか（Why）
経済学の定理を定理証明器に載せる動きは、2025〜2026年に一気に加速した。2025年には vNM 期待効用定理（arXiv:2506.07066）と Simon の限定合理性（arXiv:2507.07052）が Lean 4 で機械証明された。2026年6月には、同名の2つの EconCSLib が EC'26 の AI-EconCS ワークショップで発表された。1つは Bei らによる4万行超・1,300定理超のライブラリで、Nash 均衡、Vickrey/VCG、Myerson の最適オークション、Arrow の定理、Gibbard–Satterthwaite、Gale–Shapley の受入保留方式までを Mathlib の上でカバーする（arXiv:2606.16144）。もう1つは Garg による「LLM が Lean を書き、Lean が検査し、人と LLM が意味を判定する」ワークフローで、Roth (1982) や Edelman–Ostrovsky–Schwarz (2007) の GSP オークションを含む20本の論文を丸ごと形式化した（arXiv:2606.13306）。それ以前にも Isabelle での VCG 組合せオークションの形式化（AFP, 2015）や Coq でのダブルオークションの検証（JAR 2025）はあり、「オークション理論は形式化できる」こと自体は既に示されている。
しかし、これらのどれも粗代替性（gross substitutes）や M♮凹性、離散凸解析には触れていない。Kelso–Crawford (1982)、Hatfield–Milgrom (2005)、Fujishige–Tamura (2007) の Lean 形式化は見当たらず、Mathlib には Matroid はあるが M凸集合・劣モジュラ関数・粗代替性の定義は存在しない。一方で離散凸解析の側では、Murota が2016年に J. Mechanism and Institution Design で「M♮凹性は粗代替性と同値であり、M-L 共役性・離散分離定理・離散不動点定理から均衡の存在と価格ベクトルの束構造が出る」という形で経済学・ゲーム理論への道具立てを整理し、Fujishige–Tamura は安定結婚問題と割当ゲームを M♮凹関数で統一している。Kojima–Tamura–Yokoo (JET 2018) は制約つきマッチングで病院側選好が M♮凹なら一般化 DA が医師側耐戦略的になることを示し、Murota–Shioura は2026年4月にも多需要モデルへの上昇オークション拡張を離散凸解析で与えている（arXiv:2604.27765）。つまり、経済学側の証明はすでに「離散凸解析の言葉」で書き直され続けているのに、形式化はまだ古典的な組合せ論の言葉に留まっている。
このギャップを埋める価値は2つある。1つは、証明を共通の抽象（M♮凹関数の性質）に乗せることで、個別定理の形式化を使い回せる部品にできること。もう1つは、未解決問題の周辺で「どの仮定を落とすと何が壊れるか」を機械的に検査できるようになることだ。取引ネットワークでは完全代替性が安定結果と競争均衡の存在を保証する極大領域であることが知られており（Hatfield–Kominers–Nichifor–Ostrovsky–Westkamp, JPE 2013）、カップルつきの研修医マッチングでは安定マッチングの存在判定が強い制限下でも NP 完全である（Biró–Manlove–McBride 2014）。粗代替性の側でも、Ostrovsky–Paes Leme のマトロイド基底評価予想が Tran (2019) により n≥4 で反証され、近似版は開いたままである（Paes Leme のサーベイ §11）。仮定と結論の対応を Lean で厳密に持つことは、これらの境界を探る作業の基盤になる。本人の言葉を借りれば「離散凸解析の観点から証明を定式化すると、未解決問題に応用が効きそうな気がする」というのが出発点である。
この研究の主な貢献・期待される成果（What）
先行研究・関連ワーク
Nyx の関連する取り組み・シナジー
対象となる読者・協力者
想定される難易度・期間
キーワード・タグ
Lean 4, mathlib, mechanism design, matching theory, discrete convex analysis, M♮-concave, gross substitutes, stable matching, auction theory, Myerson, VCG, decision theory, EconCSLib, autoformalization
その他の関連リンク
連絡先・ディスカッション
contact@nyx.foundation