Anthropic이 Lean 4로 작성된 페르마의 마지막 정리의 완전한 기계검증 증명을 Apache 2.0 라이선스로 오픈소스 공개했다. 코드는 수학 라이브러리 Mathlib 위에 구축됐다. 저장소가 제시하는 형식적 명제는 다음과 같다: 임의의 n ≥ 3과 양의 정수 a, b, c에 대해 a^n + b^n ≠ c^n. 이 명제는 Lean에서 커널이 한 단계씩 검증할 수 있는 정리로 작성됐으며, 어떠한 허점도 남기지 않았다.
이 작업에서 가장 직관적으로 와닿는 부분은 규모다. 저장소 집계에 따르면 모듈 60475개, 정리 29511개, 정의 모듈 1450개이며, 익스포트 검증은 선언 1052234건을 포괄한다. 생성된 HTML 문서는 약 390MB, 전체 익스포트 파일은 37.8GB에 달한다. 로컬에서 전 과정을 재현하려면 300GB 이상의 디스크 공간과 최대 약 153GB의 메모리가 필요하다.
세 단계 검증, 모두 기록이 남았다
저장소는 단순히 “컴파일이 통과했다”는 말 한마디로 끝내지 않았다. 첫 번째 단계는 Lean 4.33.1 자체의 커널 전체 컴파일로, 96코어 머신에서 5시간 32분이 걸렸다. 두 번째 단계는 leanprover 공식 comparator 도구(v4.33.0)를 이용한 재검증으로, 약 14시간 46분이 소요됐다. 세 번째 단계는 Rust로 작성된 독립 커널 nanoda 0.4.13으로 교체해 16스레드로 약 30분 만에 Your solution is okay!라는 출력을 얻었다.
세 단계 검증 외에도 하나의 엄격한 제약이 더 있다. 모든 모듈에서 axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def, #eval가 전혀 등장하지 않아야 한다는 것이다. 이 키워드들은 Lean 커뮤니티에서 대표적인 허점으로 통한다. sorry는 말 그대로 “아직 증명되지 않았다”는 뜻이고, native_decide는 일부 판단을 커널이 검증하지 않는 기계어 코드에 넘겨버린다. 이를 모두 배제한다는 것은 증명의 신뢰도를 오롯이 Lean 커널과 검증 도구에 걸었다는 뜻이며, README 자체도 그렇게 설명하고 있다.
AI가 얼마나 작성했는지는 저장소도 밝히지 않았다
README에 따르면 Lean 소스코드는 “사람이 작성한 오픈소스 Lean 코드 위에서, Lean을 심판으로 삼아 AI 에이전트가 만들어냈다”고 한다. 정확한 비율은 공개되지 않았다. 어떤 모듈이 사람이 작성한 것이고 어떤 모듈이 모델이 생성한 뒤 커널에 의해 반려되어 다시 작성된 것인지에 대한 세부 내역은 공개 자료에서 확인할 수 없다.
반면 사람이 마련한 토대는 비교적 명확히 표시돼 있다. 기존 학술 프로젝트에서 가져온 의존 파일이 106개이며, 대부분은 임페리얼 칼리지 런던의 Kevin Buzzard가 이끄는 FLT 형식화 프로젝트와 쿠머 정칙 소수 경우를 다루는 flt-regular에서 왔다. 이와 별도로 Mathlib에 이미 있는 내용을 다시 증명한 모듈도 23개 있다.
형식수학의 역사라는 맥락에 놓고 보면 이번 규모의 도약은 두드러진다. 4색 정리는 2005년 Georges Gonthier가 Coq로 형식화를 완료했고, 케플러 추측을 다루는 Flyspeck 프로젝트는 2014년 완료가 선언됐다. 두 사례 모두 인년(person-year) 단위의 작업량이 들었다. Buzzard 팀이 FLT 프로젝트를 시작할 때도 외부의 예상은 마찬가지로 수년 규모였다. 이번 저장소가 그 결승선을 얼마나 앞당겼는지는 사람과 AI의 실제 분담 비율에 달려 있으며, 이는 현재로서는 유일하게 확인할 수 없는 숫자이기도 하다.
참고 출처: Anthropic 공개 저장소의 README 및 검증 기록, CocoLoop, Mathlib 프로젝트, 임페리얼 칼리지 런던 FLT 프로젝트 공개 자료. 모듈 수, 정리 수, 세 단계 검증 소요 시간은 저장소 기재 내용을 기준으로 확인했다.