수학 AI 스타트업 액시엄은 수학사에서 가장 방대하다고 여겨지는 '유한 단순군 분류(CFSG)'의 전체 증명을 컴퓨터로 검증했다고 밝혔다. 이 정리는 유한군을 이루는 가장 기본 단위인 유한 단순군을 모두 분류한 결과로, 약 100명의 수학자가 500편이 넘는 논문과 1만5000페이지에 걸쳐 완성했다. 액시엄은 이를 증명 보조 언어 린(Lean) 코드로 재구성했고, 수십 개의 AI 에이전트를 투입해 24일 만에 완전한 기계 검증 증명을 만들었다. 전체 결과물은 4310만 줄 규모다.
이번 작업은 문헌을 단순히 코드로 옮긴 수준에 그치지 않았다. 액시엄은 전체 증명을 108개 마일스톤과 약 380개 세부 작업으로 나누고, 에이전트들이 논문에서 논증을 찾아 코드로 변환하거나 필요한 선행 정리를 증명하도록 했다. 이 과정에서 기존 논문에 있던 중요한 오류와 누락된 가정 34건이 드러났고, 일부는 핵심 논리 수정이 필요했다. 특히 불균형 집단 정리(UGT) 관련 반례 문제는 군론 전문가와의 협의를 거쳐 대체 논증으로 보완했다. 기계 검증이 긴 수학 증명의 신뢰성을 높이고, 사람이 지나치기 쉬운 논리의 빈틈을 드러내는 도구임을 보여준 사례다.