액시엄, 1만5000쪽 유한 단순군 분류 증명을 기계 검증
수학 AI 스타트업 액시엄이 유한 단순군 분류 정리의 전체 증명을 컴퓨터가 검증할 수 있는 형태로 재구성했다고 밝혔다. 이 정리는 500편이 넘는 논문과 약 1만5000쪽에 걸쳐 약 100명의 수학자가 완성한 것으로, 액시엄은 수십 개 AI 에이전트를 투입해 24일 만에 검증을 마쳤다고 설명했다.
증명 보조 언어 린을 사용한 결과는 4310만 줄의 코드로 만들어졌다. 108개 마일스톤과 약 380개 작업으로 나누고 에이전트들이 논문을 코드로 옮기며 선행 정리와 의존 관계를 확인했다. 이 과정에서 기존 문헌의 오류와 누락된 가정 34개도 발견했다.
기계 검증은 각 논리 단계가 앞선 가정에서 실제로 도출되는지 확인하는 데 강점이 있다. 다만 형식화된 명제가 원래 의도한 수학적 의미를 담는지는 사람이 따로 검토해야 한다. 이번 사례는 AI 에이전트가 대규모 학술 문헌을 분담해 형식화하고 오류를 찾는 연구 보조 도구가 될 가능성을 보여준다.