Claude, 11일 만에 Lean으로 페르마의 마지막 정리를 형식화하다
Anthropic은 Claude가 1,300만 줄의 Lean 코드를 작성해 페르마의 마지막 정리에 대한 최초의 완전한 컴퓨터 검증 증명을 만들어냈다고 밝혔다.
목차 · 11
Anthropic은 9월 4일 Claude가 페르마의 마지막 정리에 대한 최초의 완전한 컴퓨터 검증 증명을 만들어냈다고 발표했다. 회사에 따르면 수십 개의 Claude 에이전트가 11일 동안 대부분 자율적으로 작업해 약 1,300만 줄의 Lean 코드를 생성하고 30,300개의 정리를 증명했으며, 이 가운데 약 29,500개가 최종 증명에 포함됐다.
이는 통상적인 수학적 의미에서 페르마의 마지막 정리에 대한 새로운 증명은 아니다. Andrew Wiles와 Richard Taylor는 1990년대에 인정받는 인간의 증명을 완성했다. Claude는 대신 문헌에 확립된 경로를 컴퓨터가 논리 단계를 검증할 수 있는 형식 언어로 옮겼다.
이 구분은 중요하다. 이 결과는 페르마의 마지막 정리가 참인지에 관한 본질적으로 새로운 지식을 더하지 않지만, 이전에는 수년간의 전문 작업이 필요할 것으로 예상됐던 고급 수학의 한 체계를 AI 시스템이 형식화할 수 있음을 보여준다. 별도의 형식화 프로젝트를 이끄는 Imperial College London의 수학자 Kevin Buzzard는 Anthropic의 코드를 컴파일하고 Comparator 검사를 실행했다. 그는 이 증명이 검증된다고 보고했다.
1. Claude가 형식적으로 증명한 것
페르마의 마지막 정리는 정수 지수 \(n\)이 3 이상일 때 양의 정수 \(a\), \(b\), \(c\)가 \(a^n+b^n=c^n\)을 만족하지 않는다는 명제다. 이 명제는 초등적이지만, 알려진 증명은 타원 곡선, 모듈러 형식, 갈루아 표현, 변형 이론, 대수기하학, 정수론과 관련된 정교한 결과에 의존한다.
Anthropic의 저장소는 최종 정리를 Lean의 자연수 위에서 직접 표현한다. 이 명제는 양의 자연수 \(a\), \(b\), \(c\)와 \(n \geq 3\)을 받아 해당 방정식이 성립할 수 없음을 증명한다. 별도의 최종 검사는 이 정리로부터 Mathlib에 이미 존재하는 페르마의 마지막 정리 명제를 도출한다.
논증은 Frey, Serre, Ribet, Wiles, Taylor–Wiles의 작업, 특히 Henri Darmon, Fred Diamond, Richard Taylor가 1995년에 제시한 해설을 따른다. 페르마 방정식의 가정적 해와 Frey 타원 곡선 사이의 연결을 사용한 뒤, 모듈러성과 레벨 하강 결과를 적용해 모순을 얻는다.
Buzzard는 구성의 중요한 세부 사항을 지적했다. Anthropic의 Wiles 기반 경로는 소수 지수 \(p \geq 17\)을 다룬다. 완전한 결과에는 남은 경우를 마무리하기 위해 이전에 형식화된 정칙 소수에 관한 작업이 통합됐다. 그럼에도 결과 Lean 정리는 3 이상인 모든 자연수 지수를 포괄한다.
이 산출물은 상당한 선행 인간 작업에도 의존한다. Anthropic은 Imperial College FLT 프로젝트, flt-regular 프로젝트, Mathlib의 자료를 적용했다고 밝혔다. 그 귀속 파일은 앞선 두 프로젝트의 자료를 포함하는 파일 106개와 Mathlib 텍스트를 재현한 파일 23개를 식별한다. 따라서 이 성과는 기존 형식 수학 생태계를 AI가 주도해 통합하고 확장한 것이며, 선행 형식 수학과 독립적으로 만들어진 1,300만 줄이 아니다.
2. 멀티 에이전트 시스템이 증명을 관리한 방법
Anthropic은 처음에 Claude 에이전트가 개별 결과는 증명할 수 있지만 더 큰 프로젝트의 맥락을 놓친다는 점을 발견했다. 에이전트들은 작업을 중복했고, 완성된 정리를 효과적으로 재사용하지 못했으며, 증명이 커지면서 협업을 중단했다. 실패한 시도도 최종 비보일러플레이트 코드의 약 7%를 차지한다.
성공한 실행에는 Columbia University의 Tianyi Peng과 협력자들이 개발한 개방형 협업 형식화 플랫폼 Prove2Me가 사용됐다. Prove2Me는 프로젝트를 정리 명제의 방향 비순환 그래프로 표현한다. 에이전트는 미완성 노드를 선택하고, 선행 조건을 증명하며, 그래프의 다른 곳에서 생성된 결과를 재사용할 수 있다.
이 플랫폼은 정리 명제와 그 증명을 분리하기도 한다. 이 설계는 재컴파일 비용을 줄이고, 모든 종속 명제를 방해하지 않고 증명을 변경하거나 교체할 수 있게 한다. 정리 노드에 첨부된 자연어 설명은 에이전트가 커져 가는 라이브러리를 검색하고 유용한 의존성을 식별하는 또 다른 방법을 제공한다.
Claude Code 기반 멀티 에이전트 하니스는 11일간의 실행 동안 수십 개 에이전트를 조율했다. 인간의 수학적 입력은 에이전트를 Jacobian으로 향하게 하거나 Mazur의 작업과 관련된 정리를 완성하도록 요청하는 등 가끔의 고수준 우선순위 지시에 국한된 것으로 알려졌다. 내부 로그에는 루트 정리가 8월 18일 증명된 것으로 기록됐다.
Anthropic은 이 실행이 대략 60억 개의 출력 토큰을 소비했다고 보고했다. Claude Fable 5.1과 대략 비슷하다고만 설명된 내부 범용 연구 모델을 사용했으므로, 정확한 모델과 구성은 공개되지 않았다. 회사는 프로젝트의 금전적 비용이나 컴퓨팅 비용을 공개하지 않았다.
완성된 개발물의 탐색 가능한 문서에는 29,511개의 정리 페이지와 1,450개의 정의 모듈이 포함돼 있다. Anthropic은 최종 의존성 경로에 궁극적으로 필요하지 않았던 결과를 포함해 더 넓은 실행 전반에서 30,300개의 컴퓨터 검증 가능 정리를 집계한다.
3. 증명이 검증된 방법
형식 증명은 정리 명제, 허용되는 가정, 검증 절차가 통제될 때에만 가치가 있다. Anthropic의 저장소는 프로젝트를 Lean 4.33.1과 Mathlib 4.33.0에 고정하고 여러 겹의 검증을 포함한다.
첫째, 프로젝트는 처음부터 빌드됐다. 60,475개 모듈은 Lean 커널의 검사를 받았다. 최종 정리는 명제적 외연성, 고전적 선택, 몫의 건전성이라는 정확히 세 가지 표준 Lean 공리에 의존한다. 배포된 증명 모듈에는 미완성 sorry 플레이스홀더, 새로 선언된 공리, 안전하지 않은 코드, 네이티브 결정 단축 경로, 외부 구현이 없다.
둘째, 프로젝트는 Lean Comparator를 사용해 증명된 정리를 Mathlib만을 기반으로 별도 제공된 챌린지 명제와 비교했다. 이 검사는 해법이 동일한 명제를 증명하고, 승인되지 않은 공리를 사용하지 않으며, 커널이 이를 수용하는지 확인하도록 설계됐다. Comparator는 수용 판정을 반환했다.
셋째, nanoda라는 독립 Lean 커널 구현이 내보낸 환경 버전을 검사하고 1,052,234개의 선언을 오류 없이 수용했다. Anthropic은 nanoda에 네 개의 패치를 적용했다. 하나는 진행 상황 출력용이고, 세 개는 정의적 동치 검색을 가속하기 위한 것이다. 저장소는 이들 패치 중 어느 것도 타입 규칙을 변경하거나 약화하지 않는다고 밝힌다.
Buzzard는 가장 관련성 높은 외부 확인을 제공했다. 그는 96코어 장비에서 코드를 컴파일하고 Comparator를 직접 실행했다. 그는 저장소가 1,340만 줄을 넘으며 Lean의 수학 라이브러리보다 컴파일에 거의 20배 더 오래 걸렸다고 설명했다.
모든 검사를 재현하는 것은 가능하지만 하드웨어 요구량이 크다. Anthropic이 문서화한 빌드는 병렬 작업 96개에서 5시간 32분이 걸렸고, 메모리 사용량은 최대 153 GB에 달했으며 Lean 빌드에 약 67 GB, 제거 가능한 생성 C 파일에 최대 220 GB를 사용했다. Comparator 실행에는 14시간 46분이 걸렸고 최대 230 GB에 달했다. 두 번째 커널을 위해 환경을 내보내면 37.8 GB 파일이 생성됐다.
이러한 검사는 나열된 공리로부터 정확한 형식 명제가 따라온다는 점을 확립한다. 이는 적어도 하나의 검사 커널과 주변 검증 도구가 정확하다는 가정하에서다. 그러나 모든 중간 정리의 기계 생성 이름이 수학적 의미를 정확히 설명하는지를 자동으로 확립하지는 않는다. Anthropic은 주요 수학 단계를 정확한 Lean 명제에 매핑하는 증명 경로 문서로 이 한계를 다룬다.
4. AI 보조 수학에서 달라진 점
이 결과 이전에 페르마의 마지막 정리는 Freek Wiedijk가 오랫동안 유지해 온 주목할 만한 정리 형식화 과제 100개 목록에 남아 있던 항목이었다. Imperial College 프로젝트는 2024년에 5년간의 자금 지원을 받아 시작됐으며, 처음에는 정리를 1980년대 말까지 알려진 결과로 환원하는 것을 목표로 했다. 프로젝트 자료는 완전한 형식화를 위해 수천 쪽의 비형식 수학을 번역해야 할 것이라고 언급했다.
Anthropic의 증명은 대신 처음부터 끝까지 최종 정리에 도달한다. Buzzard는 이것이 자신의 프로젝트를 불필요하게 만들지는 않는다고 강조했다. Imperial의 노력은 재사용 가능하고 사람이 읽을 수 있는 Mathlib 확장을 개발하며, 더 현대적인 증명을 따른다. Anthropic은 자신의 저장소를 유지보수하지 않고 기여를 받지 않는 연구 산출물로 규정한다.
따라서 실질적 진전은 처리량에 있다. Claude의 에이전트들은 대수학, 조화 해석, 기하학, 정수론 전반의 형식 정의와 증명을 Mathlib의 줄 수를 5배 이상 초과하는 규모로 조립했다. 이 결과는 그래프 기반 에이전트 시스템이 단일 모델 컨텍스트로는 감당하기 어려울 만큼 큰 형식화에서 의존성을 유지하고 작업을 조율할 수 있음을 보여준다.
이 증명은 AI 생성 수학을 위한 검증 경로도 보여준다. 언어 모델은 설득력 있는 산문으로 잘못된 자연어 논증을 생성할 수 있지만, Lean은 타입 검사를 통과하지 못하는 증명 항을 거부한다. 별도로 통제된 정리 명제와 Comparator는 에이전트가 문제를 몰래 약화하거나 변경해 성공할 위험을 추가로 줄인다.
이 메커니즘이 수학자의 필요성을 없애지는 않는다. 인간은 여전히 형식 명제가 의도한 개념을 포착하는지 결정하고, 결과의 중요성과 서술을 평가하며, 재사용 가능한 라이브러리를 유지해야 한다. 그러나 정의, 정리 명제, 신뢰할 수 있는 검증 경계가 독립적으로 점검된다면, 논리 단계의 철저한 검사를 인간 심사자에서 증명 보조기 커널로 옮길 수 있다.
자주 묻는 질문
Claude가 페르마의 마지막 정리에 대한 새로운 증명을 발견했나요?
아니요. Lean이 모든 논리 단계를 검사할 수 있도록 Frey–Serre–Ribet–Wiles–Taylor–Wiles 문헌에 확립된 경로를 형식화했습니다.
이 결과는 독립적으로 검증됐나요?
Kevin Buzzard는 공개 코드를 컴파일하고 Lean Comparator를 실행해 검증된다고 보고했습니다. 저장소에는 Lean과 독립 nanoda 커널의 성공적인 검사 기록도 있습니다.
어떤 Claude 모델이 증명을 생성했나요?
Anthropic은 정확한 공개 모델명을 밝히지 않았습니다. 내부 범용 연구 모델을 Claude Fable 5.1과 대략 비슷하다고 설명합니다.
연구자들이 검증을 재현할 수 있나요?
네, 코드와 지침은 Apache 2.0 라이선스로 공개돼 있습니다. 완전한 재현에는 일부 검증 단계에서 수백 GB의 메모리를 포함한 상당한 하드웨어가 필요합니다.
1,300만 줄 저장소는 모두 AI가 새로 작성한 수학인가요?
아니요. AI 에이전트는 Mathlib과 Imperial College FLT 및 flt-regular 프로젝트의 기존 오픈소스 형식화 작업을 바탕으로 개발물 대부분을 생성하고 통합했습니다.
참고 자료
Share