Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem

技术摘要：使用 Aristotle API 对跳蚤问题的形式化案例研究

问题陈述
本文呈现了“跳蚤问题”的形式化案例研究，该问题最初是第 50 届国际数学奥林匹克（IMO 2009）的第 6 题。该定理指出：对于任意 $n$ 个互不相同的正整数集合 $\{a_1, \dots, a_n\}$ 以及一个包含 $n-1$ 个正整数的集合 $M$（其中总和 $\sum a_i \notin M$），存在一种跳跃顺序的排列 $\sigma$，使得没有任何中间部分和 $S_k = \sum_{i=1}^k a_{\sigma(i)}$ 落在 $M$ 中。该问题因其历史难度而著称，在 2009 年 IMO 所有题目中平均得分最低，且需要涉及排列和禁止集的非平凡组合推理。

方法论
本研究利用 Aristotle API，这是一个自动化定理证明系统，结合了语言模型引导的搜索、非形式化引理生成以及基于 Lean 4 证明助手（使用 Mathlib）的形式化。作者向 Aristotle API 提供了特定提示，要求其提供跳蚤问题的严格、完整证明，明确禁止将该问题作为已知定理引用，并要求构建有效的排列。

生成的产物是一个 Lean 4 项目，其中包含该定理的广义版本（允许 $|M| < n$ 而非严格等于 $n-1$，并允许 $0 \in M$）。作者对生成的代码进行了细致检查，以区分完全通过机器验证的声明与包含未解决证明占位符（sorry）的声明。

主要结果与已验证组件
生成的 Lean 开发并未产生主定理的完整证明。相反，它形成了一个混合产物，包含四个完全验证的辅助引理和一个未解决的主定理：

1. 已验证的局部组件：

   • PS last：验证了最终部分和等于跳跃的总和。
   • PS swap：验证了相邻跳跃的对换仅影响该位置特定的中间部分和，而保持其他部分和不变。
   • PS swap eq：验证了对换后部分和的代数形式（$S_k' = S_k - a_{\sigma(k)} + a_{\sigma(k+1)}$）。
   • maximizer swap in M：验证了局部极大性论证。它确立了：如果某个排列最大化特定的得分函数 $G(\sigma)$，且可交换位置处的部分和在 $M$ 中，则交换后产生的值也必须在 $M$ 中。

2. 未解决的全局组件：

   • 主定理 grasshopper 直接由单个 sorry 封闭。
   • Aristotle 输出摘要将缺失的步骤识别为全局计数论证。虽然局部引理确立了特定对换会强制成员资格进入 $M$，但系统未能协调这些事实以证明它们会产生至少 $n$ 个不同的禁止值，从而与假设 $|M| < n$ 相矛盾。Lean 源代码并未将主定理简化为单独的、编码的计数引理；该缺口仍是一个未证明的义务。

贡献
本文做出了两项主要贡献：

1. 可复现的产物：它提供了一个可检查、可复现的 Lean 4 形式化尝试，用于解决一个困难的奥林匹克组合数学问题，使用了 Aristotle API，包括完整的源代码和运行日志。
2. 对 AI 局限性的精确分析：它提供了对 AI 生成证明的“证据状态”的详细剖析。研究表明，AI 系统可以成功验证局部、代数和基于交换的推理步骤，但在执行关闭主定理所需的全局组合记账方面失败。

意义与主张
本文论证了“已验证声明”与“由 sorry 封闭的声明”之间的区别对于解释 AI 辅助定理证明至关重要。本案例研究的意义在于它展示了局部证明搜索可以成功，而全局推理仍然未解决。

作者强调，包含 sorry 的 Lean 文件成功编译不足以作为证明完成的证据。该产物作为一个警示性示例：虽然 AI 工具可以生成大量已验证的数学发展（如四个辅助引理），但它们仍可能留下证明的核心逻辑引擎（即全局矛盾）未实现。本文得出结论：可信的 AI 辅助形式化需要严格检查证明义务和依赖关系，而不能仅仅依赖生成代码的存在。