Lean 4에서 AI 지원 정리 증명을 위한 Aristotle API 활용: Grasshopper 문제의 형식화 사례 연구

AI 지원 정리 증명 (AI-assisted theorem proving)은 이제 올림피아드 수준의 수학을 위한 상당한 양의 Lean 개발물을 생성할 수 있지만, 이러한 개발물의 증거적 상태는 어떤 선언 (declarations)이 실제로 검증되었는지에 달려 있습니다. 본 논문은 원래 IMO 2009 Problem 6으로 제시되었던 Grasshopper 문제에 대해 Aristotle API 증명 시도를 Lean 4로 형식화 (formalization)한 사례 연구를 보고합니다. 생성된 결과물 (artifact)은 정리의 일반화된 Lean 버전을 기술하고, 극대성 (maximality) 및 인접 스왑 교환 (adjacent-swap exchange) 전략의 국소적 구성 요소에 대한 4개의 검증된 보조 보조정리 (helper lemmas)를 포함하며, 메인 정리는 하나의 해결되지 않은 sorry에 의해 직접적으로 닫힌 상태(closed)로 남겨둡니다. 검증된 구성 요소들은 최종 부분합 (partial sum)이 전체 합과 같다는 점, 인접 치환 (adjacent transposition)이 관련 중간 부분합에만 영향을 미칠 수 있다는 점, 변경된 부분합이 기대되는 형태를 가진다는 점, 그리고 인접한 후속 스왑을 허용하는 위치에서의 극대성이 그에 상응하는 금지 집합 (forbidden-set) 멤버십 사실을 강제한다는 점을 확립합니다. Aristotle 출력 요약은 의도된 남은 수학적 단계로, 이러한 멤버십 사실들이 적어도 n개의 서로 다른 금지된 값들을 생성하여 기수 가정 (cardinality assumption) |M| < n과 모순됨을 보여주는 데 필요한 전역적 카운팅 단계 (global counting step)를 식별합니다. Lean 소스 자체는 메인 정리를 별도로 인코딩된 카운팅 보조정리 (counting lemma)로 축소하지 않습니다. 이 사례 연구는 AI 지원 형식화 (AI-assisted formalization)의 핵심적인 한계, 즉 정리에 필요한 전역적 조합론적 장부 정리 (global combinatorial bookkeeping)는 해결되지 않은 채 국소적 증명 탐색 (local proof search)만 성공할 수 있다는 점에 대한 조사 가능한 사례를 제공합니다. 본 논문은 재현 가능한 Lean 결과물과 검증된 증명 내용 및 검증되지 않은 증명 내용에 대한 정밀한 분석을 기여합니다.