Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
人工智能
2026-05-20 v1 计算机科学中的逻辑
摘要
AI 辅助定理证明现已能为奥林匹克级别的数学问题生成大量的 Lean 开发内容，但此类开发内容的证据效力取决于哪些声明被实际验证。本文报告了一项 Lean 4 形式化案例研究，针对 Aristotle API 对“蚱蜢问题”（原题为 IMO 2009 第 6 题）的一次证明尝试。生成的产物陈述了该定理的一个广义 Lean 版本，包含四个已验证的辅助引理，分别对应极大性和相邻交换策略的局部组成部分，而主定理 grasshopper 则直接以一个未解决的 sorry 结束。已验证的部分确立了：最终部分和等于总和、相邻对换仅影响相关的中间部分和、改变后的部分和具有预期形式，以及在允许相邻后继交换的位置上的极大性会强制产生一个对应的禁集成员关系事实。Aristotle 输出摘要指出，预期的剩余数学步骤是全局计数步骤，用以证明这些成员关系事实会产生至少 n 个不同的禁止值，从而与基数假设 |M| < n 矛盾；Lean 源代码本身并未将主定理归约到一个单独编码的计数引理。本案例研究提供了一个可检验的实例，揭示了 AI 辅助形式化中的一个核心局限：局部证明搜索可以成功，而定理所需的全局组合簿记工作仍未解决。本文贡献了一个可复现的 Lean 产物，并对其已验证和未验证的证明内容进行了精确分析。
引用
@article{arxiv.2605.20120,
title = {Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem},
author = {Gabriel Rongyang Lau},
journal= {arXiv preprint arXiv:2605.20120},
year = {2026}
}