수학 AI 기업 Axiom은 자사의 AxiomProver 에이전트 군집이 유한 단순군 분류 정리(CFSG)의 Lean 형식화를 24일 만에 마쳤다고 발표했다. 회사는 이 정리에 대한 최초의 완전한 컴퓨터 검증 증명이라고 주장한다. 코드는 GitHub에 Apache-2.0 라이선스로 공개됐다. 저장소에는 최종 버전에 sorry 자리표시자가 없고 native_decide도 쓰지 않았으며, 명제 외연성, 고전적 선택 공리, 몫의 건전성이라는 세 가지 표준 공리에만 의존한다고 명시돼 있다.
유한 단순군 분류는 흔히 "대칭성의 주기율표"로 불린다. 모든 유한 단순군은 18개의 무한 족 가운데 하나에 속하거나 26개의 산재군 중 하나라는 내용이다. 원래 증명은 500편이 넘는 논문, 약 1만 5천 쪽에 걸쳐 있으며, 약 100명의 수학자가 1955년 무렵부터 2004년까지 써 내려갔다. 마지막 조각인 quasithin 부분은 Aschbacher와 Smith의 것으로, 한 편만 1221쪽에 달한다.
24일 동안 벌어진 일
Axiom이 공개한 과정에 따르면, 프로젝트는 10월 1일에 협업용 Slack 워크스페이스를 만들었고 10월 2일에 첫 에이전트들이 가동됐다. 전체 증명은 108개의 마일스톤과 약 380개의 작은 작업으로 쪼개졌다. 에이전트들은 GitHub 이슈에서 작업을 맡고 Slack에서 진행 상황을 보고했다. 주도 에이전트가 문제 분할과 명제 검토를 맡았고, 나머지 에이전트는 기존 결과를 검색하거나 Lean 증명을 작성했으며, 전제가 부족하면 다시 아래로 작업을 넘겼다.
과정이 순탄하지는 않았다. 초기에 작성된 코드 한 묶음은 암묵적 가정에 오류가 있어 통째로 삭제됐고, 팀은 계획을 다시 짰다. 이후에는 빌드 속도가 병목이 되었는데, 엔지니어들이 캐싱과 병렬 검사를 도입하고 유한 계산을 검증 가능한 증명서로 외부화해 전체 빌드 시간을 24시간 이내로 줄였다. 10월 10일에는 프로젝트와 별도로 Monster 군이 단순군임을 증명했다고 먼저 발표했다.
말뭉치와 관련해 Axiom은 논문과 서적 715편을 읽어 들였고, 앞선 Qiuzhen-CFSG 프로젝트의 코드 약 120만 줄과 Mathlib, Tau Ceti 같은 기존 형식화 라이브러리도 재사용했다고 밝혔다.
덤으로 찾아낸 오류
형식화 과정에서 팀은 비교적 뚜렷한 수학적 편차 34건을 기록했다. 가장 주목받는 사례는 "불균형군 정리"(UGT) 경로에 있다. Walter가 1986년 회고록에 쓴 닫힘 관련 주장에 반례가 있는데, PSL₂(49)에서 출발하면 PSL₂(7)에 이르게 되며 후자는 바로 그 족에서 제외된 군이다. Aschbacher와 Smith의 보조정리 하나에서도 SL₂(5) 반례가 발견됐고, 등식을 부등식으로 바꾸면 뒤따르는 논증도 확장해야 한다.
Axiom은 이를 위해 35쪽짜리 논문을 따로 발표해 대체 논증을 제시했고, Lyons와 Solomon 등 자문위원이 참여해 이 경로를 보완했다. 회사는 이 반례들이 UGT 자체를 뒤집지 않으며, 분류 정리를 흔드는 것은 더더욱 아니라고 거듭 강조한다.
"the classification remains the achievement of the mathematicians who discovered the groups"
(분류는 이 군들을 발견한 수학자들의 업적으로 남는다.)
이전의 기계 검증과 비교하면
가장 자주 비교 대상이 되는 것은 Gonthier 팀이 2012년 Coq에서 완료한 홀수 위수 정리 검증이다. 이 정리는 Feit와 Thompson이 1963년에 쓴 255쪽짜리 논문에서 나왔고, 프로젝트에는 약 6년이 걸렸으며 분류 증명을 떠받치는 초석 중 하나다. 이번 Axiom은 건물 전체를 다루었고, 걸린 시간은 일 단위로 센다.
둘의 속도를 곧바로 비교할 수는 없다. 홀수 위수 프로젝트는 당시 라이브러리를 거의 맨바닥에서 쌓았지만, Axiom은 Mathlib과 앞선 120만 줄의 CFSG 코드 위에 서 있었고, 에이전트 수는 "수십 개"였다. 그 뒤의 연산 자원, 하드웨어, 총비용은 공개되지 않았고 투입 인시도 밝히지 않았다. 24일은 형식화 프로젝트 자체의 기간이며, 그것이 기대고 있는 수십 년의 인간 작업은 포함하지 않는다.
몇 가지 유보 사항도 분명히 적혀 있다. 프로젝트 메타데이터는 검토를 "자체 평가"로 표시했고, 깨끗한 환경에서 전체 빌드를 재현한 제3자는 아직 없다. 기계 검사가 보장하는 것은 적어 둔 가정에서 추론이 성립한다는 점뿐이며, 분류 진술의 정의가 원래 정리에 충실한지는 군론 학자들이 하나하나 대조해야 한다. UGT 논문은 동료 심사를 하지 않는 프리프린트 플랫폼에 올라와 있고, 정오표는 프로젝트 페이지에 게시할 것이라고 Axiom은 밝혔다.
형식화 분야 종사자에게 다음으로 볼 것은 두 가지다. 커뮤니티가 이 4310만 줄을 독립적으로 돌려 볼 수 있는지, 그리고 34건의 편차 가운데 원저자 측이 몇 건을 확인해 줄지다.
참고 출처: Axiom 프로젝트 공지 및 GitHub 저장소, Unite.AI, CocoLoop, Kingy AI. Lean 코드 줄 수, 선언 수, 마일스톤 수, 편차 건수는 Axiom이 공개한 수치를 따랐으며, 홀수 위수 정리 검증 기간은 Microsoft Research 자료에 근거한다.