수학 AI 스타트업 액시엄(Axiom)이 수학사에서 가장 방대하고 복잡한 증명으로 꼽히는 ‘유한 단순군 분류(CFSG·Classification of Finite Simple Groups)’ 전체를 컴퓨터로 검증하는 데 성공했다. ‘대칭의 주기율표’라고도 불리는 이 체계는 약 100명의 수학자가 500편이 넘는 논문과 1만5000페이지에 걸쳐 완성했다. 액시엄은 이를 AI 에이전트와 증명 보조 도구로 다시 구성했으며, 기존 문헌에서 오류와 누락된 가정도 찾아 수정했다.
액시엄은 26일(현지시간) 수십 개의 AI 에이전트를 투입해 24일 만에 CFSG의 완전한 기계 검증 증명을 구축했다고 발표했다.
수학 명제와 논증을 컴퓨터가 확인할 수 있도록 표현하는 증명 보조 언어 ‘린(Lean)’을 사용했으며, 개발 결과물은 총 4310만 줄의 코드에 이른다.
CFSG는 유한군을 이루는 가장 기본적인 단위인 ‘유한 단순군’을 모두 분류한 정리다. 군론(Group Theory)은 대칭성을 수학적으로 다루는 분야이며, 유한 단순군은 유한군을 더는 분해할 수 없을 때의 기본 구성 요소다. CFSG는 이러한 기본 요소를 모두 밝혀낸 정리로, 방대한 증명 분량 때문에 수학계에서 ‘거대 정리(The Enormous Theorem)’라고도 불린다.
이번 프로젝트는 방대한 수학 문헌을 코드로 옮기는 데 그치지 않았다. 논증의 각 단계를 컴퓨터가 검증하게 만드는 과정에서 기존 논문에 담긴 중요한 오류와 누락된 가정 34개를 찾아냈다. 대부분은 오탈자, 표의 오류, 빠진 가정 등이었지만, 일부는 증명의 핵심 논리를 고쳐야 하는 문제였다.
대규모 증명을 효율적으로 완성하기 위해 액시엄은 여러 AI 에이전트가 동시에 작업하는 스웜(Swarm) 시스템을 만들었다. 증명 전체를 108개 마일스톤과 약 380개의 세부 작업으로 나누고, 에이전트들이 깃허브와 슬랙을 통해 업무를 배정받고 결과를 공유하도록 했다.
에이전트들은 기존 논문에서 관련 수학적 논증을 찾아 린 코드로 바꿨다. 또 다른 에이전트들은 필요한 선행 정리를 증명하거나, 각 결과가 전체 증명에 필요한 조건과 맞는지 점검했다. 인간 수학자와 엔지니어는 복잡한 수학적 난제를 살피고 작업 구조와 검증 시스템을 개선했다.
초기에는 일부 작업이 증명되지 않은 가정을 전제로 삼는 문제가 생겼다. 액시엄은 그런 가정에 의존해 작성한 수만 줄의 코드를 지우고 작업을 다시 설계하기도 했다. 이후 세부 정리를 더 작은 단위로 나누고, 각 결과가 최종 정리와 어떻게 연결되는지 분명히 하는 방식으로 작업을 개선했다.
코드 검증 속도도 중요한 과제였다. 여러 에이전트가 코드를 빠르게 작성했지만, 린이 전체 의존성을 다시 확인하는 데 시간이 걸렸기 때문이다. 액시엄은 여러 작업자의 검증 결과를 공유하고, 수정되지 않은 코드의 검사 결과를 재사용하는 시스템을 구축했다. 덕분에 검증을 병렬로 진행하고 반복 계산을 줄일 수 있었다.
기계 검증의 주요 성과 중 하나는 기존 수학 문헌의 오류를 발견한 것이다. 사람은 논문을 읽으며 문맥이나 수학적 직관으로 생략된 부분을 보완할 수 있지만, 컴퓨터는 증명에 필요한 가정과 논리적 연결을 명시해야 한다. 그 과정에서 기존 논증의 문제가 드러났다.
액시엄에 따르면 발견된 오류 중 상당수는 오탈자, 표의 오류, 가정 누락처럼 비교적 사소한 문제였다. 하지만 일부 논증은 수정이 필요했다. 예를 들어 군론의 특정 성질을 다룬 논문에서 두 수학적 값이 같다는 주장이 반례와 모순되는 것으로 나타났다. 해당 주장을 부등식으로 바꾸자 후속 논증에서 추가로 따져야 할 경우가 생겼고, 연구진은 이를 다루도록 증명 구조를 보완했다.
가장 어려운 문제 중 하나는 유한 단순군 분류의 핵심 결과인 ‘불균형 집단 정리(UGT)’를 증명하는 과정에서 발견됐다. 액시엄은 기존 증명의 일부 주장이 성립하지 않는 반례를 찾아냈고, 이를 해결하기 위해 군론 전문가들과 논의해 대체 논증을 개발했다.
이 과정에서 액시엄의 AI 시스템은 군론의 새로운 결과도 도출했다. 연구진은 관련 부분군 구조를 비교하면서 특정 조건에서는 단순군의 구조가 보존된다는 정리를 증명했다. 이후 기존 1세대 증명 방식으로 UGT를 더 짧게 이끌어낼 수 있는 방법도 확인했다.
액시엄은 발견한 오류와 수정 내용을 정리해 군론 연구자들이 활용할 수 있도록 공개할 예정이다. 이번 성과는 기존 증명의 문제를 찾는 데서 그치지 않고, 필요한 논증을 보완하고 새로운 증명 경로를 마련했다는 점에서도 의미가 있다.
린은 수학적 정의와 명제, 증명을 컴퓨터가 확인할 수 있는 형식으로 작성하는 프로그래밍 언어다. 사람이 쓴 증명을 린으로 옮기면 각 단계가 앞선 가정과 정리에서 논리적으로 도출되는지 기계적으로 검사할 수 있다. 다만 형식화한 명제가 실제로 의도한 수학적 주장을 담고 있는지는 사람이 따로 확인해야 한다.
대규모 수학 증명을 기계로 검증하려는 시도는 이번이 처음은 아니다. 2012년에는 조르주 곤티에가 이끈 연구진이 코크(Coq) 증명 보조 도구를 사용해 유한 단순군 분류의 토대가 된 페이트-톰프슨 정리를 형식화했다. 액시엄의 이번 프로젝트는 그보다 훨씬 방대한 CFSG 전체 증명을 대상으로 했다는 점에서 다르다.
유한 단순군 분류는 추상대수학뿐 아니라 수학적 물리학에서도 쓰인다. 가장 큰 유한 단순군인 몬스터군(Monster group)은 특정 양자 이론의 대칭성과 연결되며, ‘괴물 문샤인(Monstrous Moonshine)’이라는 수학적 관계를 통해 모듈러 함수와도 연관된다. 괴물 문샤인은 현대 수학에서 겉보기에는 전혀 관련이 없어 보이는 두 거대한 수학 개념이 기적처럼 연결되어 있음을 뜻하는 정리다. 이처럼 CFSG는 여러 수학 분야의 결과가 의존하는 중요한 토대다.
이번 프로젝트는 AI 에이전트들이 방대한 수학 문헌을 나눠 형식화하고, 기계 검증으로 오류를 발견하며, 필요할 때는 새로운 논증까지 구성할 수 있음을 보여준다.
액시엄은 CFSG의 증명과 의존 관계를 컴퓨터가 확인할 수 있는 형태로 정리했다. 연구자들은 개별 정리의 가정과 논리적 연결을 직접 살펴보고, 검증된 결과를 후속 연구에 활용할 수 있게 됐다.