Anthropic, 페르마의 마지막 정리를 Lean 4로 완전히 증명하다
Fermat's Last Theorem in Lean 4
Anthropic이 페르마의 마지막 정리에 대한 완전하고 기계가 검증한 증명을 Lean 4로 공개했습니다. 이 증명은 Frey, Serre, Ribet, Wiles, Taylor-Wiles의 논증을 따르며, Mathlib 위에 구축되었습니다. 60,475개의 모듈이 Lean 커널로 검증되었고, 독립적인 Rust 기반 커널 nanoda로도 재검증되었습니다. 증명은 표준 공리만 사용하며, 저장소에는 브라우저에서 탐색할 수 있는 HTML 버전과 증명 경로를 설명하는 PROOF-PATH.md가 포함되어 있습니다.
함께, 이러한 검사들은 위의 명제가 세 가지 공리로부터 따라 나온다는 것을 확립합니다. 단, Lean 커널(또는 nanoda)과 검사 도구에 대한 신뢰가 전제됩니다.