AI가 만든 수학 결과를 믿을 수 있는지 묻는 일은, 답이 그럴듯한지와 증명이 실제로 성립하는지를 나눠 보는 데서 시작한다. Anthropic은 2026년 9월 4일, Claude가 Lean으로 페르마의 마지막 정리를 끝까지 형식화했고 컴퓨터 검사를 통과했다고 공개했다.
페르마의 마지막 정리는 n이 2보다 클 때 양의 정수 a, b, c가 an + bn = cn을 만족하지 않는다는 명제다. 1995년 앤드루 와일스의 증명이 나온 뒤에도, 사람이 읽는 증명을 컴퓨터가 한 단계도 건너뛰지 않고 검사할 수 있는 Lean 코드로 옮기는 일은 수년짜리 프로젝트로 여겨졌다. Anthropic에 따르면 Claude는 11일 동안 대부분 자율적으로 작업해 Lean 코드 약 1,300만 줄을 만들었고, 최종 증명에는 중간 정리 29,500개가 쓰였다.
이번 결과는 새 정리 발견보다 증명 검사에 가깝다
이 작업의 출발점은 와일스와 리처드 테일러의 증명 계열이다. Claude가 새로운 수학 명제를 처음 찾아냈다는 발표와는 다르다. 이미 알려진 논증을 Lean이 읽을 수 있는 형식으로 바꾸고, 그 논증이 목표 정리까지 끊기지 않게 이어지는지를 검사 가능한 산출물로 만든 것이다.
그 차이는 실무의 코드 리뷰와도 닮았다. 문서에 적힌 설계 설명은 사람이 맥락을 읽어야 판단할 수 있지만, 타입 검사와 테스트는 정해진 규칙 안에서 실패 지점을 바로 드러낸다. 형식화된 증명은 후자에 가깝다. 사람이 생략했던 자명한 단계도 Lean에서는 명시해야 하며, 앞 단계 하나가 닫히지 않으면 다음 단계로 넘어갈 수 없다.
Lean이 확인하는 범위는 어디까지인가
Lean의 검사는 입력된 정리 문장, 사용한 공리, 그리고 그 사이를 잇는 모든 형식 단계에 적용된다. 공개 저장소의 FinalCheck.lean은 페르마의 마지막 정리가 Lean의 표준 공리 세 개에만 의존하도록 확인하고, 비교 도구는 이 정리 문장이 Mathlib에 있는 페르마 정리 문장과 일치하는지도 검사한다. 저장소는 별도 Rust 구현인 nanoda가 같은 환경의 내보내기를 받아들였다고도 기록한다.
따라서 이 결과가 주는 답은 분명하다. AI가 작성한 결과라도 문제를 형식 언어로 충분히 표현하고, 사용하는 전제와 규칙을 고정할 수 있다면 결론까지의 논리 연결은 기계가 반복해서 확인할 수 있다. 반대로 어떤 전제를 채택할지, 형식화 대상이 원래 연구 질문을 제대로 담았는지, 사람에게 이해되는 설명이 되었는지는 Lean의 통과 표시만으로 결정되지 않는다.
다중 에이전트의 병목은 계산량보다 작업 기억이었다
초기 시도에서는 여러 에이전트가 어느 정리가 끝났는지와 다음 작업이 무엇인지를 잃어버려 협업이 흐트러졌다고 Anthropic은 설명한다. 최종 증명에 남은 비정형 코드 중 약 7%는 이 실패한 시도에서 왔다. 전환점은 Tianyi Peng 연구진이 만든 Prove2Me였다.
Prove2Me는 정리 문장을 방향성 비순환 그래프로 유지한다. 에이전트는 아직 증명되지 않은 정리와 이미 재사용할 수 있는 정리를 그래프에서 찾아 병렬로 맡는다. 정리의 문장과 증명 본문을 다른 파일로 나눠 Lean 컴파일 비용을 줄이고, 각 정리에 자연어 설명을 붙여 검색과 재사용도 돕는다. Anthropic은 Claude Code 기반 다중 에이전트 하네스와 이 구조를 함께 써 약 60억 출력 토큰을 소비했다고 밝혔다.
AI 결과의 검증 비용을 줄이는 방식
AI가 더 많은 증명과 분석을 만들수록, 전문가가 처음부터 끝까지 읽어 확인하는 방식만으로는 검토량을 따라가기 어렵다. 이번 사례가 보여 주는 것은 모델의 답을 곧바로 신뢰하는 방법이 아니라, 답을 검증기가 다룰 수 있는 산출물로 바꾸는 방법이다. 수학에서는 Lean 코드가 그 매개이고, 소프트웨어에서는 재현 가능한 빌드와 테스트, 데이터 분석에서는 입력 데이터와 변환 기록이 같은 역할을 할 수 있다.
중요한 것은 AI의 결과물 옆에 검사 가능한 흔적을 남기는 일이다. 결론만 받는 흐름에서는 검토자가 결과와 추론을 함께 복원해야 한다. 반면 정리 그래프, 형식 증명, 고정된 공리처럼 검증 경로를 남기면 새 결과를 더 빠르게 걸러내고 기존 작업 위에 이어 쌓을 수 있다.
출처: Anthropic, Formalizing Fermat’s Last Theorem · anthropics/fermats-last-theorem