Lean中组合博弈的形式化研究
速览
研究者使用Lean定理证明器对组合博弈进行形式化建模与验证，展示了Lean在数学证明自动化中的应用潜力。这项工作有助于将抽象数学理论转化为可验证的计算机代码，为AI辅助数学推理提供新工具。组合博弈的形式化还能启发强化学习中的策略学习与搜索算法设计。
AI 深度解读
背景
组合博弈论（Combinatorial Game Theory）研究的是两人零和、完美信息、有限步的博弈。这类博弈没有随机性，没有平局，且必然在有限步内结束，最后无法行动的一方判负。经典的例子包括 Nim、Hackenbush 和 Chomp。与之相反，扑克包含随机元素，国际象棋可能出现和棋，而 Borel 确定性理论中的 Gale–Stewart 博弈可以无限进行下去——这些都不属于组合博弈的范畴。
Lean 4 是一个交互式定理证明器，近年来被广泛用于数学形式化。该项目（Combinatorial Games in Lean）旨在将组合博弈论的核心内容用 Lean 4 进行形式化，从而为后续研究提供可验证的数学基础。
核心内容
该项目计划形式化四大类内容：
- 一般组合博弈理论：包括温度（temperature）、被支配位置（dominated positions）、可逆位置（reversible positions）等核心概念。
- 特定组合博弈理论：例如偏序集博弈（poset games）、Hackenbush、井字棋（tic‑tac‑toe）等具体实例的分析。
- Nimbers（尼姆数）理论：证明 Nimbers 构成代数闭域，并证明最简扩张定理（simplest extension theorems）。
- 超现实数（Surreal Numbers）理论：建立超现实数的域结构，并证明它们可以表示为 Hahn 级数。
该形式化工作主要基于 Conway（2001）的经典著作 On Numbers and Games，同时参考了多部现代资料：
- Conway, J. H. – On Numbers and Games (2001)
- Dierk Schleicher 与 Michael Stoll – An Introduction to Conway's Games and Numbers (2005)
- Siegel, A. N. – Combinatorial Game Theory (2013)
项目仓库地址位于 GitHub，目前已经包含了对上述主题的部分形式化工作，并仍在持续补充。
关键要点
- 组合博弈定义明确：两位玩家（Left 和 Right）交替行动，信息完全公开，游戏必须在有限步内终止，无行动者输，无平局。
- 形式化的目标覆盖从基础理论（温度、支配关系）到具体博弈（井字棋、Hackenbush）再到深层数学结构（Nimbers 的代数性质、超现实数的 Hahn 级数表示）。
- 形式化依赖的文献以 Conway (2001) 为核心，兼顾现代研究成果，确保方法与定义的准确性和前沿性。
- 该项目为组合博弈论在交互式定理证明器中的落地提供了可复用的代码库，也为其他数学领域的形式化提供了参考范例。
意义与影响
形式化组合博弈论不仅能够验证已有定理的正确性，还能帮助发现潜在的错误或遗漏。Lean 4 的严格类型系统迫使研究者将每一个定义和证明都精确无误地写出，从而加深对理论细节的理解。
此外，该项目将经典数学结构（如 Nimbers、超现实数）与计算机辅助证明结合，为数学教育、博弈 AI 的可信推理、以及更一般的数学形式化运动提供了具体案例。随着项目逐步完善，未来可能成为组合博弈论研究的标准参考实现。