AI-assisted theorem proving can now generate substantial Lean developments for olympiad-level mathematics, but the evidential status of such developments depends on which declarations are actually verified. This paper reports a Lean 4 formalization case study of an Aristotle API proof attempt for the Grasshopper problem, originally posed as IMO 2009 Problem 6. The generated artifact states a generalized Lean version of the theorem, contains four verified helper lemmas for local components of a maximality and adjacent-swap exchange strategy, and leaves the main theorem grasshopper closed directly by one unresolved sorry. The verified components establish that the final partial sum equals the total sum, that an adjacent transposition can affect only the relevant intermediate partial sum, that the changed partial sum has the expected form, and that maximality at a position admitting an adjacent successor swap forces a corresponding forbidden-set membership fact. The Aristotle output summary identifies the intended remaining mathematical step as the global counting step needed to show that these membership facts produce at least n distinct forbidden values, contradicting the cardinality assumption |M| < n; the Lean source itself does not reduce the main theorem to a separately encoded counting lemma. This case study gives an inspectable example of a central limitation in AI-assisted formalization, namely that local proof search can succeed while the global combinatorial bookkeeping required for a theorem remains unresolved. The paper contributes a reproducible Lean artifact and a precise analysis of its verified and unverified proof content.

翻译：AI辅助定理证明现可为奥林匹克级别数学问题生成规模可观的Lean代码，但此类代码的证成性取决于哪些声明实际通过了验证。本文报告了针对Aristotle API尝试证明蝗虫问题（原IMO 2009第6题）的Lean 4形式化案例研究。生成的工件陈述了该定理的广义Lean版本，包含四个已验证的辅助引理，分别对应极大性与相邻交换策略的局部组件，而主定理“grasshopper”则直接通过一个未解决的“sorry”闭合。已验证组件建立了以下结论：最终部分和等于总和、相邻对换仅影响相关中间部分和、变化后的部分和具有预期形式，以及允许相邻后继交换位置上的极大性强制对应禁止集成员事实。Aristotle输出摘要指出预期剩余数学步骤为全局计数步骤，需证明这些成员事实产生至少n个不同禁止值，从而与基数假设|M|<n矛盾；而Lean源码本身并未将主定理归结为独立编码的计数引理。本案例研究提供了一个可检验的实例，揭示了AI辅助形式化的核心局限：局部证明搜索可成功执行，而定理所需的全局组合簿记仍悬而未决。本文贡献了可复现的Lean工件，并对其已验证与未验证的证明内容进行了精确分析。