1만5천 쪽 수학 증명, 액시엄이 컴퓨터 검증 코드 공개

수학 AI 기업 액시엄 매스(Axiom Math)가 약 1만5천 쪽에 걸친 유한단순군 분류 정리(CFSG)의 증명을 컴퓨터로 검증할 수 있는 코드로 공개했다고 밝혔다. 10월 26일자 발표에 따르면 수학자와 엔지니어가 수십 개 AI 에이전트를 지휘해 24일 동안 증명 보조 도구 Lean용 코드 약 4,310만 줄을 만들었다.

이번 작업은 여러 수학자가 쌓아 올린 기존 분류 증명을 형식 언어로 옮겨 연결한 것이다. 액시엄은 문헌과 다른 처리가 필요했던 주요 사례 34건을 해결했다고 설명했다. 중요한 보고는 사람이 조사했고, 원래 분류 연구에 참여한 리처드 라이언스와 로널드 솔로몬에게도 자문했다.

공개 코드가 목표로 삼은 명제는 모든 유한단순군이 명시적으로 구성한 목록 속 어느 군과 구조적으로 같다는 내용이다. 참조한 타우 세티(TauCeti) 파일은 순환군·교대군·리형 군·산재군의 구체적인 대상을 모아 이 명제를 정의한다. 이 파일 자체는 분류의 증명문이 아니라 증명해야 할 목표를 기록한 것으로, 전체 개발이 무엇을 보이려 하는지 읽는 출발점이다. 여기서 구조가 같다는 동형 관계는 원소의 이름이 달라도 군의 연산이 대응한다는 뜻이다. 명제는 조건을 충족하는 모든 유한단순군을 대상으로 한다.

중간 논증의 결함은 별도 경로로 보완

함께 공개한 논문은 불균형 군 정리(UGT)에 이르는 기존 논증의 한 단계를 집중적으로 다룬다. 특정 연산 뒤에도 관련 단순군이 정해진 범위에 남는다는 주장을 반례가 깨뜨렸다. 논문은 이것이 UGT 자체나 해당 중간 명제의 결론을 뒤집은 반례는 아니라고 명시한다. 결함이 확인된 추론을 다른 근거로 연결하는 것이 과제였다.

논문은 솔로몬의 1976년 이론을 토대로, 분류에 필요한 단순군의 경우를 다루는 대체 논증을 제시한다. 특정 가정 아래 비교를 반복해도 관련 단순 몫군을 보존한다는 결과가 정리 2.3이다. 이후 사람이 찾은 더 짧은 경로는 주석 9.5에 실렸다. 긴 논증은 AI가 형식화한 경로와 추가 보존 결과를 보여 주기 위해 유지했다.

배포물은 GitHub에서 아파치 2.0 라이선스로 공개됐다. 저장소 설명에 따르면 Lean 4.35.0-rc3와 기존 수학 라이브러리 Mathlib·TauCeti에 기반하며, 증명을 비워 두는 표식 없이 표준 공리를 사용한다. 회사는 계산을 네이티브 코드로 실행해 판정하는 기능에도 의존하지 않았다고 적었다. 이는 배포자가 밝힌 검증 구성이다.

전체 프로젝트를 다시 만드는 명령도 공개했다. 다만 액시엄은 빌드 도구 Lake의 공개 변경 사항과 향후 원본 프로젝트에 반영할 최적화를 적용해 빌드 시간을 24시간 미만으로 줄였다고 설명한다. 이 수치는 회사가 사용한 구성의 결과다. AI Ping은 공개 설명과 지정된 명제 파일을 대조했으며, 전체 증명을 직접 재빌드하지는 않았다.

Lean의 공식 검증 문서는 화면의 개별 정리 확인과 그 정리가 불러오는 전제의 확인을 구분한다. 앞서 가져온 결과에 증명이 비어 있는 부분이 있어도 현재 정리의 논리 전개는 통과할 수 있다. 문서는 정리가 의존하는 공리를 추적하고, 컴파일된 증명을 별도 검사 도구로 다시 확인하는 절차를 설명한다.

검증할 문장이 의도한 수학을 표현하는지도 별도로 살펴야 한다. 기계는 주어진 정의와 전제에서 결론이 나오는지를 확인한다. 따라서 코드의 논리적 유효성을 확인하는 작업에는 그 코드가 가리키는 정의와 명제를 읽는 검토가 함께 따른다. 공개 저장소의 증명과 명세를 제3자가 조사할 때도 이 두 확인 대상이 남는다.

증명 웹사이트에서는 초기 작업 계획과 Lean 저장소를 구분해 살펴볼 수 있다. 논문별·단계별 관계, 각 명제의 의존 관계를 탐색하고 검색하는 화면을 제공한다. 반면 정오표 페이지는 10월 28일 확인 시점에도 군론 연구자들과 목록을 정리한 뒤 공개하겠다고 안내했다. 발표에서 언급한 수정 사례 전체를 내려받을 수 있는 단계와는 구별된다. 사이트가 집계한 논문·책은 715개, 정의와 정리 등을 포함한 선언은 약 205만 개다. 관계도에서는 코드 줄 수와 명제 수, 출처별로 표시 방식을 바꿀 수 있다. 큰 증명 속에서 한 결과가 어떤 문헌과 앞선 결과에 연결되는지 찾아보도록 구성했다.