Axiom Math, 4,310만 줄 규모의 Lean 군 분류 증명 공개

Axiom Math는 2026년 10월 27일, 수십 명의 AI 에이전트 군집을 지휘한 엔지니어와 수학자들이 24일 동안 작업해 Lean 증명 보조기에서 약 4,310만 줄의 코드를 작성한 결과물인, 유한 단순군 분류에 대한 최초의 완전한 컴퓨터 검증 증명이라고 자사가 부르는 것을 공개한다고 밝혔다.

회사는 발표문에서 “오늘 유한 단순군 분류(Classification of Finite Simple Groups, CFSG)에 대한 최초의 완전한 컴퓨터 검증 증명을 공개합니다”라고 밝혔다. 이 분류는 유한군의 기본 구성 요소를 규명하며, 원래 증명은 약 100명의 수학자가 500편이 넘는 논문에 걸쳐 작성한 약 15,000쪽 분량에 이른다. 이 규모 때문에 이 증명은 ‘거대한 정리’라는 별칭을 얻었다.

Axiom이 공개한 내용

CFSG에 따르면 모든 유한 단순군은 소수 차수의 순환군이거나, 기호가 최소 5개인 교대군이거나, 유한체 위에 구성된 16개 무한 계열의 리형 군 중 하나이거나, 정확히 26개의 고립된 산발 단순군 중 하나다. 발표문은 일부 저자가 Tits 군을 27번째 군으로 세기도 한다고 덧붙였다. 가장 큰 산발 단순군인 Monster는 1980년 Robert Griess가 차원 196,884의 대수를 사용해 구성했다.

사람이 수행한 증명 작업은 수십 년에 걸쳐 이어졌다. 1963년 Walter Feit와 John Thompson은 모든 비가환 유한 단순군의 위수가 짝수임을 증명했으며, 이 내용은 Pacific Journal of Mathematics 한 호 전체를 채운 255쪽짜리 논문으로 발표됐다. Daniel Gorenstein은 1972년 분류를 완성하기 위한 16단계 계획을 제시했고, 1983년에는 완성됐다고 선언했다. 그러나 준박형 경우는 Geoffrey Mason이 작성한 미완성 원고에 의존하고 있었으며, Michael Aschbacher와 Stephen Smith가 2004년 1,221쪽 분량의 연구를 발표하면서 비로소 해결됐다. 이로써 ‘1세대 증명’으로 알려진 작업이 마무리됐다. Gorenstein과 Richard Lyons가 시작하고 나중에 Ronald Solomon과 Inna Capdeboscq가 합류한 더 체계적인 2세대 증명은 아직 완성되지 않았다. 이에 Axiom은 1세대 증명을 형식화했다.

프로젝트 페이지는 이 형식화가 1세대 증명을 따르며 모든 논리적 단계를 Lean 커널이 검증한다고 설명하고, Lean 코드 4,310만 줄, 선언 205만 개, 자료에 포함된 논문과 서적 715권을 제시한다. Axiom은 증명 지도를 작성할 때 2세대 연구 자료를 참고했으며, 이번 형식화에는 기존 Qiuzhen-CFSG 프로젝트의 코드 약 120만 줄이 포함됐다고 밝혔다. 또한 수백 명의 기여자가 참여한 Mathlib을 기반으로 구축했다. 프로젝트는 핵심 기여자로 Dean Cureton, Vasily Ilin, Bhavik Mehta, Niels Voss를 꼽고, 총괄 연구책임자로 Letong Hong을 명시했다.

공개 GitHub 저장소는 이 결과물을 `sorry`를 사용하지 않은 Lean4 증명이라고 설명하며, 버전 4.35.0-rc3으로 고정하고 Mathlib 및 TauCeti 프로젝트를 기반으로 구축했다고 밝힌다. 또한 `native_decide`를 사용하지 않고 `Classical.choice`, `propext`, `Quot.sound`라는 표준 공리만 사용한다. TauCeti에서 가져온 분류의 형식적 명제는 다음과 같다. “모든 유한 단순군은 분류 목록에 명시적으로 구성된 군 중 하나와 동형이다.” README에 따르면 `lake build`는 개발 내용을 전체적으로 검증한다. 또 Lake 빌드 도구에 대한 공개 변경 사항과 팀이 상위 프로젝트에 반영할 계획인 최적화를 적용해 빌드 시간을 24시간 미만으로 줄였다. 코드는 Apache-2.0 라이선스를 적용한다.

24일간 이어진 에이전트 군집 작업

2026년 10월 1일, Axiom은 프로젝트를 조율하기 위해 Slack 채널을 개설했다. 기존 Lean 작업과 출판된 문헌을 바탕으로 내부에서 작성한 증명 지도를 활용해 전체 작업을 108개 마일스톤과 약 380개의 세부 과제로 나눴다. 첫 에이전트 군집은 2026년 10월 2일 가동됐으며, 에이전트들은 GitHub 이슈를 통해 마일스톤을 맡고 완료한 작업을 Slack에 보고했다. 주요 에이전트는 어려운 논증을 세분화하고 명제를 검토했으며, 다른 에이전트들은 기존 결과를 찾거나 Lean 증명을 작성했다. 에이전트는 누락된 선행 조건을 다른 에이전트에게 맡길 수도 있었고, 그 결과는 공유 저장소에 반영됐다.

초기 진행 과정에서 취약한 지점이 드러났다. 겉보기에는 처리하기 쉬운 일부 마일스톤에 에이전트들이 증명하지 않고 가정한 방대한 선행 조건이 숨어 있었다. 이에 팀은 그런 가정에 기반한 코드 수만 줄을 삭제하고 더 타당한 계획에 따라 다시 작업을 시작했다. 초기 마일스톤 중 하나는 신호화자 함자 정리와 관련된 것이었는데, 후보 증명은 정당화가 필요한 구조적 가정에 의존했다. 에이전트들이 Lean이 재검증할 수 있는 속도보다 빠르게 증명을 만들어 내면서 빌드 시간도 병목이 됐다. Axiom에 따르면 엔지니어들은 캐시된 빌드 결과를 여러 작업자에게 분산하고, 독립적인 검증을 병렬로 실행했으며, 비용이 많이 드는 유한 계산을 별도로 검증할 수 있는 인증서로 분리했다. 회사는 이러한 변경으로 검증 속도가 몇 자릿수 규모로 향상됐다고 밝혔다.

Axiom은 2026년 10월 10일 채널에 에이전트들이 Monster가 단순군임을 증명했다는 메시지가 올라왔다고 전했다. 에이전트들은 Griess 대수를 통해 Monster의 존재를 형식화하고, Monster형 군을 Monster와 동일시하는 정리도 형식화했다. 2026년 10월 13일에는 마일스톤 하나만 완료됐다. 이에 엔지니어들은 계획을 다시 세우고 미완료 마일스톤을 더 작고 정확하게 서술된 정리들로 나눴다. 각 분해 과정에서는 짧은 Lean 증명을 통해 세부 정리들이 원래 마일스톤을 어떻게 성립시키는지 보여야 했다.

출판된 증명에서 발견된 공백

증명을 Lean으로 옮기는 과정에서 발표된 논증의 문제점이 드러났다고 Axiom은 전했다. 대부분은 오탈자, 표의 오류, 가정 누락 등 사소한 문제였지만, 회사는 발표된 기록과 다른 주목할 만한 사례가 34건이라고 집계했다. 그중 가장 중대한 사례는 불균형 군 정리(Unbalanced Group Theorem, UGT)와 관련되어 있다.

한 가지 사례는 Aschbacher와 Smith의 준박형 군 관련 저서에서 발견됐다. 한 보조정리는 두 수량이 같다고 주장했다. 에이전트들은 군 SL₂(5)와 관련된 반례를 찾아냈는데, 해당 등식이 2를 요구하는 상황에서 한 수량의 값은 1이었다. 등식을 부등식으로 바꾸자 보조정리가 바로잡혔지만, 이후의 논증에서는 경우를 배제하는 데 등식이 사용됐으므로 연구팀은 앞선 논증의 범위를 넓혀 해당 구성들도 다루도록 했다.

UGT는 부분군에 관한 정보를 바탕으로 전체 군을 식별하는 데 도움을 준다. 함께 공개된 논문의 초록에 따르면, 분류 정리의 귀납적 가정 아래에서 대합의 중심화 부분군에 정규인 자명하지 않은 홀수 차수 부분군이 존재하면, 그 부분군이 속한 단순군은 홀수 표수의 리형 군이거나 특정 차수의 교대군이어야 한다. Axiom은 John Walter의 1986년 회고록을 바탕으로 UGT에 접근했다. 이 논증을 형식화하던 중 에이전트들은 논증에서 사용된 폐쇄성 주장에 대한 명시적 반례를 발견했다. 즉, 관련 단순군들을 지정된 족 안에 유지한다고 가정한 연산이 그 족에서 명시적으로 제외되는 군을 만들어낼 수 있었다.

회사의 설명에 따르면, 체 대합의 중심화 부분군이 PGL₂(7)인 PSL₂(49)에서 출발하면 이 연산은 단순 성분 PSL₂(7)을 만들어낸다. 7이 메르센 소수이므로 PSL₂(7)은 해당 족에서 제외된다. Axiom은 이 반례들이 UGT 자체는 물론, Walter의 명제 II.5.9(ii)의 결론조차 반박하지는 않는다고 덧붙였다.

이 수정에는 Solomon의 1976년 최대 2-성분 이론이 활용됐다. Axiom에 따르면, 이 이론은 AxiomProver 시스템이 만들어 형식화한 대안적 논증의 핵심 아이디어를 제공했다. 논문에서 정리 2.3(단순 톱의 보존)으로 제시된 핵심 단계는 AxiomProver가 증명한 군론의 새로운 결과라고 Axiom은 설명한다. 이 결과는 Gilman과 Solomon의 축약, Foote와 Harris의 인식 정리와 결합되어 분류에 필요한 UGT의 단순군 형태를 제공한다. 형식화가 끝난 뒤 Axiom의 수학자들은 1세대 방법론만으로 정리 2.3 없이도 같은 결론에 이르는 더 짧은 추론을 찾아냈으며, 이를 비고 9.5에 기록했다.

Colin Defant와 Ken Ono가 기고한 이 논문, 《불균형 군 정리》는 CC BY 4.0 라이선스에 따라 2026년 10월 27일 Hexagon 프리프린트 서버에 버전 1로 게시됐다. 프로젝트 페이지에는 논문 분량이 35쪽으로 나와 있다. Axiom은 문헌에서 발견된 정오 사항을 취합하기 위해 군론 연구자들과 협력 중이며, 이를 프로젝트의 정오표 페이지에 공개할 예정이라고 밝혔다. 분류의 토대가 된 연구를 수행한 Lyons와 Solomon은 UGT 수정 과정에서 자문을 제공했다. 회사는 두 사람과 외부 자문위원 Dan Nakano를 포함한 자문위원회와 함께 정오 사항을 계속 검토하고 해결해 나가겠다고 밝혔다. Axiom은 증명을 기계적으로 검증할 수 있게 하고, 발견한 장애물을 기록하며, 이를 해결하는 형식화된 논증을 제공한 것이 자사의 기여라고 설명하면서도, 이 군들을 발견하고 논증을 발전시킨 수학자들이 이룬 성과가 분류 정리의 업적이라고 밝혔다.