利用 Aristotle API 进行 Lean 4 中 AI 辅助定理证明：蚱蜢问题的形式化案例研究

本文研究了利用 Aristotle API 在 Lean 4 中对 IMO 2009 第 6 题（蚱蜢问题）进行的 AI 辅助定理证明形式化。生成的代码包含四个经验证的辅助引理，确立了局部极大性与相邻交换策略的关键性质，但主定理因缺失全局计数步骤而未完全证明。该案例揭示了当前 AI 形式化的核心局限：局部搜索虽能成功，却难以解决定理所需的全局组合簿记问题。文章提供了可复现的 Lean 工件及对已验证与未验证内容的精确分析。