Axiom, CFSG Lean 형식화 24일 완수 발표: 4,310만 줄 규모

핵심 요약

AI 수학 스타트업 Axiom은 2026년 10월 26일 유한 단순군 분류 정리(CFSG)의 Lean 형식화를 24일 만에 완수했다고 발표했다 (Axiom 공식 글). Axiom은 "The largest math proof in human history is now computer-verified."라고 주장한다 (AI타임스 인용). 이 글의 수치는 모두 Axiom 자체 발표 기준이다. 공식 글에는 외부 독립 검토 언급이 없다.

용어 정리

• 단순군: 군론은 대칭을 다루는 수학이다. 단순군은 더 쪼갤 수 없는 대칭 구조다. CFSG는 이를 모두 분류하며 "대칭의 주기율표"로 불린다.
• Lean과 형식화: Lean은 증명을 한 단계씩 기계로 검사하는 언어다. 형식화는 사람이 쓴 증명을 Lean 코드로 옮기는 일이다.
• 원 증명 규모: AI타임스는 "약 100명의 수학자, 500편 이상의 논문, 약 15,000쪽"이라고 전했다.

방법론

1. 에이전트 swarm과 작업 분할

Slack 채널은 10월 1일 열렸고 첫 에이전트 swarm은 10월 2일 가동됐다. 리드 에이전트, 검색 에이전트, 증명 작성 에이전트 수십 개가 여러 모델을 섞어 일했다. 정확한 수는 공개되지 않았다. 작업은 108개 마일스톤과 380개 규모(공식 표기 approximately 380)의 세부 태스크로 나뉘었다. 에이전트는 GitHub 이슈로 태스크를 가져갔다. 10월 13일 마일스톤 1개를 마친 뒤 재계획했다.

2. 1세대 증명과 검증 가속

2세대 증명이 미완성이라 1세대 증명을 형식화했다. 출판 문헌 기반의 내부 proof map으로 의존성을 관리했다. 빌드 캐싱, 분산 검증, 유한 계산의 외부화(certificate)로 검증을 앞당겼다. 결과는 Lean 코드 4,310만 줄이며 Qiuzhen-CFSG 120만 줄이 포함된다.

3. 기록과의 차이 34건

발표된 기록과 주목할 차이가 34건 나왔다. 대부분 오타, 표 오류, 누락된 가정이다. 가장 큰 건은 Unbalanced Group Theorem(UGT)이다. SL2(5) 관련 반례로 거짓인 보조정리가 확인됐고, Walter의 UGT 증명 속 closure 주장에도 반례가 있었다. Axiom은 대체 논증과 새 정리 "preservation of simple tops"(Theorem 2.3), Remark 9.5의 더 짧은 유도를 제시했다.

의의와 비교

인간 수학자가 주요 보고를 조사했고 Richard Lyons, Dan Nakano, Ron Solomon이 외부 자문을 맡았다. 전체 증명, 의존성 그래프, errata는 cfsg.axiommath.ai에, 코드는 GitHub(AxiomMath/CFSG)에 공개됐다. 누구나 오류 기록과 증명 구조를 직접 열람할 수 있다는 점이 실용적 의의다.

장점과 한계

장점은 공개성과 오류 발견이다. 증명 전체와 errata가 열려 있고, 문헌의 누락된 가정이 드러났다.

한계는 Axiom 공식 글이 직접 경고한다. Lean은 증명되지 않은 추가 가정에 의존한 결과도 검증할 수 있어 진척이 과장되기 쉽다. 정리 진술이 올바르게 명세됐는지는 사람이 확인해야 한다. 일부 역사적 증명과 UGT 경로가 다르고, errata와 문헌 작업은 진행 중이다. 즉 기계 검증은 명세된 진술이 증명됐다는 뜻이지, 그 진술이 원래 정리와 같다는 보장까지는 아니다.

전망

저장소와 proof map이 공개돼 외부 수학자가 진술 명세와 의존성을 점검할 수 있다. 독립 검토 결과가 나오기 전에는 "검증 완료"를 확정된 사실로 보기 어렵다. 같은 방식이 다른 대형 증명에 통할지는 공개된 자료로는 알 수 없다.

결론

Axiom의 발표는 AI 에이전트 분업으로 대형 증명 형식화를 짧은 기간에 진행한 사례다. 방법과 결과물이 공개된 점은 평가할 만하다. 다만 수치는 자체 발표이고 진술 명세는 사람이 확인해야 한다. 수학 형식화와 AI 에이전트 협업에 관심 있는 연구자와 개발자에게 추천하며, 독립 검토 소식을 함께 확인하길 권한다.