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)과 검사 도구에 대한 신뢰가 전제됩니다.
HN 토론
32- black_knight
Lean 코드 중 일부가 기존 Lean 라이브러리에 기여할 수 있는 형태인지 궁금합니다.
제 경험상 Fable이 다른 사람들이 작업할 수 있는 형식화 라이브러리에 적합한 코드를 작성하게 하려면 많은 인간의 입력이 필요합니다. 하지만 여기에는 분명히 많은 선행 조건들도 함께 형식화되어 있으므로, 모든 노력이 하나의 정점 증명에만 낭비되지 않으면 좋겠습니다!
(이전 댓글의 재게시이지만, 여기에 더 잘 어울리는 것 같습니다.)
- superposeur
증명의 가치 중 상당 부분은 그로텐디크 스타일로 목표에 도달하는 데 필요한 수학적 정의와 중간 정리를 개발하는 데 있습니다. 이러한 능력은 여전히 AI의 범위를 벗어나는 것 같습니다(적어도 최근 AI 증명의 홍수 속에서 '스킴'이나 '모듈러 형식'과 같은 근본적으로 새롭고 유용한 정의가 나왔다는 소식은 듣지 못했습니다). 하지만, AI가 큰 Lean 증명을 효율적으로 리팩터링하여 Lean 조각들로 만든 다음, 그 조각들을 다시 인간이 이해할 수 있고 매력적인 이름을 가진 새로운 정의로 해석하는 과정을 통해 이 기술도 개발할 수 있을지 궁금합니다.
- mcapodici
정말 살아있음을 느끼게 하는 시대네요.
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
가장 짧거나, 가장 간결하거나, 가장 이해하기 쉬운 (형식적으로 검증된) 증명을 찾는 것도 흥미로운 문제, 어쩌면 더 흥미로운 문제가 될 것 같습니다.
- rawling