액시엄, 수학 사상 가장 긴 증명 '유한 단순군 분류' 기계 검증 완수

무엇을 해냈나

액시엄(Axiom)은 26일(현지시간) 수십 개의 AI 에이전트로 24일 만에 유한 단순군 분류(CFSG)의 완전한 기계 검증 증명을 만들었다고 밝혔어요.

• CFSG는 약 100명의 수학자가 500편 넘는 논문, 1만 5,000쪽에 걸쳐 완성한 정리로 '대칭의 주기율표', '거대 정리'라고도 불려요.
• 유한군을 더 쪼갤 수 없는 기본 단위인 유한 단순군을 모두 분류한 정리예요.
• 증명 보조 언어 Lean을 썼고, 결과물은 4,310만 줄이에요.

일하는 방식

• 여러 에이전트가 동시에 일하는 스웜 시스템을 만들었어요.
• 전체 증명을 108개 마일스톤, 약 380개 세부 작업으로 나누고 깃허브와 슬랙으로 배정·공유했어요.
• 에이전트는 논문의 논증을 Lean 코드로 옮기고, 선행 정리를 증명하고, 조건이 맞는지 확인했어요. 사람 수학자와 엔지니어는 어려운 장애물을 조사하고 구조를 다듬었어요.
• 초기엔 증명 안 된 가정에 기댄 코드 수만 줄을 지우고 다시 설계하기도 했어요. 변경 안 된 코드의 검사 결과를 재사용해 검증을 병렬화했어요.

찾아낸 오류

기존 논문에서 중요한 오류와 누락된 가정 34개를 찾았어요. 대부분은 오탈자, 표 오류, 빠진 가정이었지만 일부는 핵심 논리를 고쳐야 했어요. 핵심 결과인 '불균형 집단 정리(UGT)'에서 반례를 발견해 군론 전문가와 대체 논증을 만들었고, 그 과정에서 새로운 정리도 증명했다고 해요.

기사 앞부분을 읽었어요.