린(Lean) 4로 증명된 페르마의 마지막 정리

AI 요약

Anthropic이 페르마의 마지막 정리를 Lean 4 증명 보조기로 완전히 기계 검증하는 데 성공한 프로젝트를 공개했다. Frey, Serre, Ribet, Wiles, Taylor-Wiles의 증명 방식을 따랐으며, 총 60,475개 모듈이 Lean 커널을 통해 검증됐다. 독립적인 Rust 기반 Lean 커널인 nanoda로도 105만 개 이상의 선언을 오류 없이 재검증해 증명의 신뢰성을 확보했다.

핵심 포인트

• Lean 4.33.1과 Mathlib v4.33.0 기반으로 페르마의 마지막 정리 완전 기계 검증 완료
• 증명은 Frey, Serre, Ribet, Wiles, Taylor-Wiles의 접근법을 따르며, 60,475개 모듈 전체가 Lean 커널로 검증됨
• 최종 정리는 Lean 기본 공리 3개(propext, Classical.choice, Quot.sound)에만 의존하며, sorry·추가 공리·native_decide 없음
• 독립 Lean 커널 nanoda 0.4.13(Rust 기반)이 1,052,234개 선언을 오류 없이 재검증

향후 전망

• 이 프로젝트는 연구용 산출물로 유지보수나 기여는 받지 않지만, 수학 증명의 기계 검증 가능성을 보여주는 중요한 이정표로 평가됨