这个案例对做AI辅助形式化验证的团队很有参考价值——它清晰展示了当前AI在局部引理证明上的能力，以及全局推理的瓶颈，做Lean或定理证明器开发的值得点开看看。
本文报告了使用Aristotle API对IMO 2009第6题（Grasshopper问题）进行Lean 4形式化证明的案例。生成的代码包含一个广义定理的Lean版本、四个已验证的辅助引理，但主定理的证明中有一个未解决的“sorry”占位符。已验证的部分建立了局部数学性质，但全局组合计数步骤未被自动化证明覆盖。该案例揭示了AI辅助形式化的核心局限：局部证明搜索可以成功，但全局推理仍需人工介入。论文提供了可复现的Lean代码，并分析了已验证与未验证的证明内容。
Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
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.