AI가 11일 만에 끝낸 20년 수학 과제

20년 넘게 열려 있던 수학 형식화 벤치마크의 마지막 항목이 채워졌다. 앤트로픽(Anthropic)은 자사 내부 모델이 프루브투미(prove2.me) 플랫폼을 이용해 페르마의 마지막 정리(FLT)의 완전한 증명을 정리 증명 언어 린(Lean)으로 형식화했다고 9월 4일 발표했다. 같은 정리를 직접 형식화하던 연구자가 코드베이스를 넘겨받아 검증한 뒤 자기 블로그에 결과를 공개하면서 내용이 알려졌다.

무슨 일인가 — 100대 과제의 마지막 칸

페르마의 마지막 정리는 프리크 비데이크가 정리한 100대 형식화 과제 목록에서 마지막까지 남아 있던 항목이었다. 이번 형식화로 20년 된 벤치마크가 사실상 마감됐다. 다만 채택된 증명은 현대적 재구성이 아니라 1995년 다르몽·다이아몬드·테일러가 정리한 와일스와 테일러의 논증 해설판이다. 랭글랜즈·튠넬 정리와 리벳의 레벨 낮추기 정리를 경유하는 경로이며, 저장소는 갈루아 표현의 평탄 변형을 다루기 위한 폰테인 이론과 마주르의 아이젠슈타인 아이디얼 연구 일부를 함께 구현했다.

규모가 눈길을 끈다. 코드베이스는 1,340만 줄을 넘고, 96코어 장비에서 린의 표준 수학 라이브러리보다 컴파일에 20배 가까이 오래 걸린다. 검증을 맡은 연구자는 500기가바이트 램을 갖춘 장비까지 제공받아 비교 도구를 돌렸고 문제가 없다고 확인했다. 저장소 규모가 워낙 커 편집기에서 파일 사이를 오가는 것조차 버거워, 앤트로픽이 함께 제공한 HTML 문서로 탐색하는 편이 실용적이었다고 한다.

핵심 짚어보기 — 수학이 아니라 속도가 뉴스다

검증자는 이 작업이 수학적으로는 새로 알려 주는 것이 거의 없다고 잘라 말한다. 증명이 옳다는 데 대해 그는 이미 99.9% 확신하고 있었고 정수론 학계 대다수는 100% 확신하고 있었다. 형식화는 초기 문헌의 논증을 충실히 따라갔을 뿐이다.

의미는 다른 데 있다. 수천 페이지 분량의 문헌을 AI 군집이 11일 만에 종단간으로 형식화했다는 사실 자체가 자동형식화의 도달점을 보여 준다. 검증자는 자신이 5년짜리 100만 파운드 연구비를 받아 진행 중인 프로젝트를 언급하면서, 앤트로픽은 11일이 걸렸지만 비용은 더 썼을지 모른다고 덧붙였다. 그는 이 속도가 유지되면 최신 연구 결과를 발표와 동시에 형식화하는 일이 가능해지고, 기계가 논증을 훑으며 빈 곳을 가차 없이 표시하게 되면서 논문 심사의 고통이 크게 줄어들 것으로 본다. 전문가 사이에서 알려진 것으로 통하던 전제들이 실제로 무엇을 가정하고 있었는지도 드러날 것이라고 했다.

1인기업 실전 적용 포인트

• 이 사건의 교훈은 검증 가능한 산출물 설계다. 린 코드처럼 기계가 참·거짓을 판정할 수 있는 형태로 결과를 뽑으면 AI 산출물을 사람이 일일이 읽지 않아도 된다. 코드·테스트·스키마 검증처럼 자동 판정 가능한 결과물부터 자동화하라.
• 대량 병렬 작업이 통하는 영역과 아닌 영역을 구분하라. 이번 작업은 기존 문헌을 옮기는 일이라 군집 투입이 먹혔지만, 무엇을 만들지 정하는 단계는 여전히 사람 몫이었다.
• 산출물 검증 절차를 미리 정해 두라. 이번에도 제3자가 컴파일과 비교 도구로 검증한 뒤에야 결과가 인정됐다. 우리 규모에서는 테스트 통과와 재현 스크립트가 그 역할을 한다.
• 문서와 탐색 도구를 함께 내라. 코드가 커지면 코드 자체보다 읽을 수 있게 만든 문서의 가치가 커진다는 것이 이번 사례에서 그대로 드러났다.

전망과 주의점

검증자는 형식화가 끝났다고 자기 연구가 사라지는 것은 아니라고 선을 그었다. 표준 수학 라이브러리에 현대 정수론의 기본 대상을 기여하는 일과, 사람이 증명을 따라 읽을 수 있는 문서를 만드는 일은 그대로 남아 있기 때문이다. 검증 가능한 코드가 곧 이해 가능한 설명은 아니라는 지적은 AI 산출물 전반에 그대로 적용된다. 기계가 통과시킨 결과물과 사람이 납득한 결과물은 여전히 다른 물건이다.

출처: Xena (https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/)