arXiv cs.AI· Haitham Masaud Amar·· 12 小时前AI 评分29
用 AI 辅助形式化合作与竞争：2018 年规划博士论文的数学补遗
Formalizing Cooperation and Competition: An AI-Assisted Mathematical Addendum to a 2018 Planning Thesis
AI 导读
研究者用 AI 辅助为 2018 年博士论文《Strategic Trip Planning》补写数学附录，重建战略选择、合作稳定性、参与者认可与执行之间的关系，并指出原论文的 Nash-to-core 命题在未说明外部机会时定义不完整。
正文 · AI 翻译
摘要：我们提出一份 AI 辅助的数学附录，作为《战略行程规划：在竞争与合作之间取得平衡》（Amar，2018）的补充。我们重构了战略选择、合作稳定性、参与者认可与执行之间的若干选定关系。在未说明外部机会之前，该论文的“纳什到核心”命题是欠定的。我们在固定外部参与者与明确效率条件下验证了两人情形下的推论。在隔离情形下，原始示例的 TU 核心为空；其有资金支持的对应版本使用明确的外部补贴。对于单调资源模型，我们刻画了精确的融资缺口。一个在 Lean 中实现的有限协商过程被证明会终止，并满足参与者认可、联合成本不恶化，以及相对于允许的已认可移动的局部最优性。配套形式化处理了议价几何与基于遗憾的效率。一个资源博弈反例说明了为何仅凭单调性无法给出统一的无政府状态代价界。可复现计算在 44 个基于来源的实例和来自另外四个合成网络族的 96 个起始案例上，比较了有记录的启发式重构与已验证过程。接受度匹配的启发式与随机成对搜索对照为优化结果提供了背景。数学要素均为已有结果；贡献在于一条可追溯的重构，将来源陈述、明确假设、已检查证明、可执行代码与保留的反例联系起来。该研究说明了 AI 辅助调查如何将遗留研究中的工程直觉转化为精确的数学命题，其条件与计算后果可被检查和复现。
| 评论： | 24 页，4 幅图。作者 2018 年滑铁卢大学博士论文的数学附录。包含 Lean 4 形式化以及可复现的合成实验作为补充材料 |
| 主题： | 计算机科学与博弈论（cs.GT）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.29637 [cs.GT] |
| （或 arXiv:2610.29637v1 [cs.GT] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.29637 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Haitham Amar 博士 [查看电子邮件]
[v1]
2026 年 10 月 21 日星期三 12:17:57 UTC（2,405 KB）
来源：arXiv cs.AI · arxiv.org