AI 에이전트, 1만5천쪽 유한단순군 증명 24일 만에 검증

AI 수학 스타트업 액시엄(Axiom)이 사람이 쓴 증명만 약 1만 5,000쪽에 이르는 '유한단순군 분류 정리'를 AI 에이전트 군집으로 처음 완전히 컴퓨터 검증했다고 밝혔다. 액시엄은 10월 26일자 연구 게시물에서 에이전트들이 24일 동안 증명 보조기 린(Lean) 코드 약 4,310만 줄을 작성했다고 설명하고, 코드를 깃허브에 공개했다.

핵심 정리

• 액시엄은 1세대 증명 전체를 린으로 옮겼으며 규모가 약 4,310만 줄, 선언 205만 개라고 밝혔다.
• 깃허브 저장소는 증명에 'sorry'(미증명 표시)가 없고 린의 표준 공리 3개만 쓴다고 적었다.
• 작업 과정에서 기존 문헌과 어긋나는 주요 사항 34건이 나왔고, 1986년 논문의 틀린 주장도 포함됐다.

유한단순군 분류 정리란

유한단순군은 유한한 대칭을 이루는 기본 단위로, 흔히 대칭의 '주기율표'로 불린다. 분류 정리는 모든 유한단순군이 소수 차수 순환군, 교대군, 16개 리 형 군 계열, 26개 산재군 가운데 하나라는 내용이다. 산재군 중 가장 큰 것이 '몬스터군'이다.

액시엄에 따르면 이 증명은 수학자 약 100명이 쓴 500편 넘는 논문에 흩어져 있다. 대니얼 고런스틴은 1983년 분류가 끝났다고 발표했지만 이르게 나온 선언이었다. 빈틈은 2004년 마이클 애쉬배커와 스티븐 스미스가 1,221쪽 분량의 'quasithin' 군 증명을 내놓으면서 메워졌다. 더 간결한 '2세대 증명'은 아직 완성되지 않았다.

AI 에이전트는 어떻게 린 증명을 만들었나

액시엄은 작업을 108개 이정표와 약 380개 세부 과제로 나눴다. 10월 1일 슬랙 채널을 열었고 10월 2일 첫 에이전트 군집을 가동했다. 에이전트들은 10월 10일 몬스터군이 단순군임을 증명했다. 그러나 10월 13일까지 완료된 이정표가 하나뿐이어서 계획을 다시 짜야 했다.

회사는 에이전트가 "계속 바뀌는 여러 모델 조합"을 썼다고만 밝혔고, 모델 이름이나 연산 자원·비용은 공개하지 않았다. 작업은 수학 라이브러리 매스립(Mathlib)을 바탕으로 했고, 앞선 Qiuzhen-CFSG 프로젝트의 코드 약 120만 줄이 들어갔다.

깃허브 저장소는 린 v4.35.0-rc3 기준이며 Classical.choice, propext, Quot.sound 세 공리만 쓰고 native_decide는 쓰지 않는다. 라이선스는 아파치 2.0이다. 액시엄은 전체 빌드 시간을 24시간 안으로 줄이는 것이 목표라고 밝혔다.

기존 증명에서 발견된 오류

가장 큰 문제는 '불균형군 정리(UGT)' 부분에서 나왔다. 액시엄은 애쉬배커·스미스 연구의 한 보조정리가 SL₂(5)에서 성립하지 않고, 월터의 1986년 논문에 있는 닫힘 주장이 PSL₂(49)에서 깨진다고 밝혔다. 다만 두 반례 모두 정리 자체를 뒤집지는 않으며, 다른 경로로 논증을 고치고 이를 위해 새 결과도 증명했다고 덧붙였다.

분류 작업에 참여했던 군론 학자 리처드 라이언스와 론 솔로몬이 댄 나카노와 함께 이 수정 작업에 자문했다.

파이트-톰프슨에서 에이전트 군집까지

지금까지 대표적인 기록은 파이트-톰프슨 정리였다. 255쪽짜리 이 증명은 조르주 공티에 연구팀이 6년 작업 끝에 2012년 Coq로 검증했다. 액시엄의 주장은 규모가 훨씬 크고 기간은 몇 주에 그친다. 최근 AI의 수학 성과 발표가 잇따르는 가운데 나온 소식으로, 앞서 구글 에이전트 군집이 연구급 수학 증명에서 거둔 성과도 주목받았다.

전망

현재까지 모든 주장은 액시엄 측 발표이며, 외부 그룹이 증명을 다시 빌드해 확인했다는 보고는 아직 없다. 액시엄도 형식화된 명제가 의도한 정리를 정확히 담았는지 사람이 검토해야 한다고 밝혔다.

자주 묻는 질문

AI가 분류 정리를 새로 발견했나?
아니다. 액시엄은 정리 자체는 이를 증명한 수학자들의 업적이라고 밝혔다. 에이전트는 기존 증명을 기계가 검사할 수 있는 코드로 옮겼다.

증명은 독립적으로 검증됐나?
액시엄에 따르면 린 커널이 모든 단계를 검사했고 코드는 공개돼 있다. 형식 명제가 올바른지에 대한 외부 확인은 아직 보고되지 않았다.

참고 자료

• Formalizing the Enormous Theorem — Axiom(2026년 10월 26일)
• The Classification of Finite Simple Groups, formalized in Lean — Axiom
• AxiomMath/CFSG — GitHub
• Axiom Math Releases 43.1M-Line Lean Proof of Group Classification — Unite.AI(2026년 10월 27일)
• Classification of finite simple groups — Wikipedia