# Axiom, 유한 단순군 분류 증명을 Lean으로 검증

> Axiom은 약 1만5000쪽에 걸친 유한 단순군 분류 증명을 Lean으로 형식화했다고 밝혔다. 작업 중 기존 논증의 오류와 가정 누락 34건도 확인했다.

Oossa · 2026-10-28 · https://oossa.com/ko/axiom-lean

수학 AI 스타트업 Axiom이 유한 단순군 분류(CFSG)의 전체 증명을 컴퓨터가 검사할 수 있는 형태로 만들었다고 2026년 10월 26일 발표했다. 회사는 수십 개의 AI 에이전트와 수학자·엔지니어가 24일 동안 작업해 Lean 코드 약 4310만 줄을 작성했다고 밝혔다. Lean은 수학적 정의와 증명을 컴퓨터가 단계별로 확인할 수 있게 쓰는 프로그래밍 언어다.

CFSG는 유한군을 이루는 가장 기본적인 단위인 유한 단순군을 모두 분류한 정리다. 원래 증명은 약 100명의 수학자가 500편이 넘는 논문에 걸쳐 만든 것으로, 분량은 약 1만5000쪽에 이른다. Axiom은 이를 ‘대칭의 주기율표’라고 설명한다. 정리는 단순군이 소수 차수의 순환군, 교대군, 리 군의 여러 무한 계열, 그리고 26개의 예외적인 군으로 모두 분류된다고 말한다.

## 검증 과정에서 무엇이 드러났나

Axiom은 전체 작업을 108개 마일스톤과 약 380개 세부 과제로 나누고, 에이전트들이 논문 속 논증을 찾아 Lean 코드로 옮기도록 했다. 사람 연구자와 엔지니어는 어려운 수학 문제를 조사하고 작업 구조와 검증 방식을 손봤다. 초기에 증명되지 않은 가정을 전제로 작성된 코드가 발견되자 수만 줄을 지우고 다시 구성하기도 했다.

논증을 컴퓨터가 읽을 수 있게 옮기는 과정에서 기존 문헌의 중요한 오류나 누락된 가정 34건이 확인됐다. Axiom에 따르면 상당수는 오탈자나 표의 오류였지만, 일부는 핵심 논증을 손봐야 했다. 특히 분류 증명의 중요한 토대인 ‘불균형 집단 정리’에서 기존 주장과 맞지 않는 반례가 발견됐다. Axiom은 군론 전문가들과 상의해 대체 논증을 만들었고, 오류 목록을 공개할 계획이라고 밝혔다.

Axiom은 이 과정에서 군론의 새로운 결과도 증명했다고 설명한다. 다만 기계 검증은 입력된 형식적 명제와 논증의 각 단계가 논리적으로 이어지는지를 확인한다. 형식화한 명제가 수학자들이 원래 의도한 주장을 제대로 담았는지는 사람이 따로 살펴야 한다. GitHub 저장소는 Lean 4와 Mathlib, TauCeti를 바탕으로 하며, 프로젝트는 기존 CFSG의 ‘1세대 증명’을 주로 따른다고 밝힌다.

## 이전의 형식화와 무엇이 다른가

이번 작업은 수학의 깊은 증명을 컴퓨터로 검증한 첫 사례는 아니다. 2012년 Georges Gonthier가 이끈 연구진은 Coq 증명 보조 도구로 페이트–톰프슨 정리를 형식화했다. 이 정리는 CFSG의 토대가 되는 결과지만, CFSG 전체를 다룬 것은 아니었다. Axiom은 이번에 방대한 분류 정리 전체를 Lean으로 형식화했다고 밝혔다.

CFSG는 추상대수학의 여러 결과가 의존하는 분류 체계이며, 수학적 물리학에서도 관련 구조가 등장한다. 예를 들어 가장 큰 유한 단순군인 몬스터군은 모듈러 함수와 연결되는 ‘괴물 문샤인’과 관련이 있다. 완성된 형식 증명은 연구자들이 개별 결과의 가정과 연결 관계를 컴퓨터로 확인하는 데 쓸 수 있다. 다만 실제 연구에서 이 검증된 결과가 어떻게 활용될지는 아직 구체적으로 제시되지 않았다.

## 팩트

- Axiom은 2026년 10월 26일 CFSG의 Lean 형식화와 컴퓨터 검증을 발표했다.
- Axiom은 24일 동안 약 4310만 줄의 Lean 코드를 작성했다고 밝혔다.
- Axiom은 기존 문헌에서 중요한 오류와 가정 누락 34건을 확인했다고 밝혔다.
- CFSG 원래 증명은 약 100명의 수학자가 500편이 넘는 논문과 약 1만5000쪽에 걸쳐 만들었다.

## 왜 중요한가

군론 연구자는 형식화된 증명을 바탕으로 각 정리의 가정과 논리적 연결을 컴퓨터로 확인하고 후속 연구에 활용할 수 있다. 다만 형식 증명이 원래 의도한 수학적 주장을 정확히 담았는지는 사람이 확인해야 하며, 새 검증 체계가 실제 연구를 어떻게 바꿀지는 아직 알 수 없다.

## 출처 및 참고 자료

1. [액시엄, 수학 사상 가장 긴 증명 '유한 단순군 분류' 기계 검증 완수](https://www.aitimes.com/news/articleView.html?idxno=216754) – AI Times, 2026-10-28
2. [Axiom Math](https://axiommath.ai/research/the-enormous-theorem-formalized/) – Axiom Math
3. [AxiomMath](https://github.com/AxiomMath/CFSG) – AxiomMath

최종 업데이트: 2026-10-28