TL;DR
Anthropic의 연구진은 Claude가 11일 동안 대부분 자율적으로 Lean 코드를 작성해 Fermat’s Last Theorem의 완전한 컴퓨터 검증 증명을 구성했다고 밝혔습니다. Claude는 1,300만 줄의 Lean 코드와 29,500개의 중간 정리를 최종 증명에 사용했고, 전체 과정에서는 30,300개 정리를 컴퓨터 검증 형식으로 만들었습니다. 작업이 가능해진 핵심은 여러 agent가 정리의 의존 관계를 공유하도록 Prove2Me의 방향성 비순환 그래프와 파일 분리 구조를 사용한 점이며, 약 60억 개의 출력 토큰이 투입됐습니다. 이 결과의 새로움은 Fermat’s Last Theorem 자체의 새로운 수학적 증명이 아니라, 복잡한 기존 증명을 Lean이 검사할 수 있는 형태로 바꿔 AI가 만든 수학 결과와 기존 문헌의 오류 검증 부담을 낮추는 데 있습니다.
섹션별 상세
이미지 분석
이미지는 Claude가 FLT를 한 번에 증명한 것이 아니라 세 갈래의 핵심 수학 구조와 여러 중간 정리를 순차적으로 연결했다는 점을 나타냅니다. Prove2Me의 DAG는 각 정리의 선행 조건과 다음 작업을 시각화해 여러 agent가 병렬로 증명을 만들고 재사용할 수 있게 한 작업 구조와 직접 연결됩니다.
Mazur, Ribet, Wiles의 하위 정리들이 의존 관계를 따라 연결되고 최종적으로 Fermat’s Last Theorem에 도달하는 방향성 비순환 그래프입니다.
용어 해설
- 페르마의 마지막 정리(Fermat’s Last Theorem)
- — 3보다 큰 정수 n에 대해 양의 정수 a, b, c가 aⁿ + bⁿ = cⁿ을 만족할 수 없다는 정리입니다. Wiles의 증명을 바탕으로 Claude가 Lean에서 컴퓨터 검증 형식으로 옮긴 대상입니다.
- 증명 보조기(Proof Assistant)
- — 수학적 명제와 추론 단계를 형식 언어로 입력받아 논리적 연결이 공리와 규칙에 맞는지 기계적으로 검사하는 소프트웨어입니다. Lean은 모든 중간 단계를 확인합니다.
- 자동 형식화(Autoformalization)
- — 사람이 읽는 수학 증명을 컴퓨터가 검사할 수 있는 형식 언어로 변환하는 과정입니다. 이 글에서는 Claude가 자연어 수준의 지시를 바탕으로 Lean 증명 코드를 작성했습니다.
- 방향성 비순환 그래프(Directed Acyclic Graph)
- — 노드 사이의 의존 관계를 방향성 간선으로 나타내되 순환이 생기지 않도록 구성한 그래프입니다. Prove2Me는 정리와 증명의 선후 관계를 관리해 여러 Claude agent의 작업을 조정했습니다.
- Mathlib
- — Lean에서 사용하는 수학 증명 커뮤니티 라이브러리입니다. Claude의 최종 증명은 Mathlib의 FLT 관련 자원을 기반으로 했으며, 코드 분량은 Mathlib의 5배를 넘었습니다.
언급된 도구
수학 증명의 모든 논리 단계를 형식 언어로 검사하는 proof assistant
Lean에서 사용하는 커뮤니티 수학 증명 라이브러리이자 FLT 명제의 비교 기준
정리 의존 관계와 자연어 설명을 관리해 여러 agent의 수학 형식화 작업을 조정하는 협업 플랫폼
Prove2Me와 결합해 여러 Claude agent의 증명 작성과 협업을 실행한 다중 agent harness의 기반
AI 요약 · 북마크 · 개인 피드 설정 — 무료
출처 · 인용 안내
인용 시 "요약 출처: AI Trends (aitrends.kr)"를 표기하고, 사실 확인은 원문 보기 기준으로 진행해 주세요. 자세한 기준은 운영 정책을 참고해 주세요.
