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

요약

본 논문은 IMO 2009의 Grasshopper 문제를 Lean 4로 형식화하여 Aristotle API를 통한 AI 지원 정리 증명 과정을 분석한 사례 연구입니다. AI는 4개의 보조 보조정리를 검증하는 데 성공했으나, 전역적 조합론적 논리가 필요한 메인 정리는 해결하지 못한 채 'sorry' 상태로 남겨두었습니다. 이는 AI가 국소적 증명 탐색에는 강점이 있지만, 복잡한 전역적 장부 정리에는 한계가 있음을 보여줍니다.

핵심 포인트

• Aristotle API를 활용하여 Grasshopper 문제의 Lean 4 형식화 및 증명 시도 수행
• 극대성 및 인접 스왑 교환 전략과 관련된 4개의 보조 보조정리 검증 성공
• 전역적 카운팅 단계가 필요한 메인 정리는 해결되지 않은 채 'sorry'로 남음
• AI 지원 형식화가 국소적 증명에는 유효하나 전역적 조합론적 추론에는 한계가 있음을 입증