AxiomProver란? 유한단순군 분류의 린 형식화 총정리

대칭의 주기율표를 컴퓨터가 끝까지 읽다

인류 역사상 가장 큰 수학 증명이 이제 컴퓨터로 검증됐다.

유한단순군 분류 정리는 유한한 단순군이 어떤 가족으로 나뉘는지 전부 적는 정리로, Axiom은 이를 대칭의 주기율표라고 불러요. 사람이 쓴 증명은 약 15,000쪽이고, 여러 세대에 걸쳐 100명이 넘는 수학자가 쌓았어요.

Axiom은 이 증명을 Lean에서 처음부터 끝까지 자동 형식화해, 컴퓨터가 검증할 수 있는 형태로 옮겼다고 발표했어요. 사람이 읽던 긴 논증을 증명 보조기가 한 줄씩 검사하는 코드로 바꾼 작업이에요.

알려진 규모와 만드는 방식

Axiom은 자사 AI 증명기 클러스터 AxiomProver가 이 형식화를 맡았다고 해요. 공개된 숫자는 두 가지예요. Lean 코드 약 5천만 줄, 걸린 시간 24일. 역대 최대 규모의 컴퓨터 검증 수학 증명이라고 주장해요.

모델 파라미터, 학습 데이터, 클러스터 구성, 사람이 중간에서 고친 비율은 발표에 없어요. 그래서 지금은 결과물의 크기와 기간, 그리고 Lean이라는 증명 보조기를 썼다는 점까지가 확인된 사양이에요.

• 정리

  유한단순군 분류. 유한 단순군을 빠짐없이 분류하는 대형 정리예요.

• 도구

  증명 보조기 Lean 위의 완전 자동 형식화예요.

• 주체

  Axiom의 AI 증명 클러스터 AxiomProver예요.

• 주장

  컴퓨터로 검증된 수학 증명으로는 가장 크다는 발표예요.

접근, 현실적인 쓰임, 아직 열린 점

공개 빌드, 다운로드, 공식 페이지는 아직 없어요. 지금까지는 짧은 미리보기 영상과 발표만 나왔고, 프로젝트 쪽으로 안내된 도메인은 cfsg.axiommath.ai예요. 앱, API, 오픈 웨이트, 요금, 사용 한도는 알려져 있지 않아요.

쓰임은 대형 정리의 컴퓨터 검증과 기존 문헌을 Lean으로 옮기는 자동 형식화예요. 다른 증명기와의 점수 비교는 공개되지 않았어요. 5천만 줄이 독립적으로 어떻게 감사되는지, 완전 형식화의 범위에 빠진 보조정리가 없는지, 코드를 외부에서 재실행할 수 있는지는 열린 질문이에요.