샌프란시스코에 본사를 두고 수학용 AI 시스템을 구축하는 회사인 Axiom Math는 수학 역사상 가장 긴 증명으로 널리 알려진 유한 단순 그룹 분류(CFSG)에 대한 최초의 완전한 컴퓨터 확인 증명을 발표했습니다. 회사의 발표에 따르면, 엔지니어와 수학자들은 단 24일 동안 수십 개의 AI 에이전트에게 명령하여 린 증명 도우미에서 약 4,310만 줄의 코드를 생성했으며, 이전에는 수십 년 동안 약 100명의 수학자들이 쓴 500개 이상의 저널 기사에서 약 15,000페이지에 걸친 결과를 검증했습니다.
이 성과는 기계 보조 수학이 빠르게 가속화되고 AI 연구 뉴스를 추적하는 매체에서 공식적인 검증이 틈새 관행에서 첨단 기능으로 이동하는 것을 지켜본 순간에 이루어졌습니다. 이번 릴리스를 특이한 점은 규모입니다. 공식화에는 100개의 마일스톤으로 구성된 약 205만 개의 선언이 포함되어 있으며, 각 선언은 각 논리적 단계를 확인하는 신뢰할 수 있는 작은 코어인 Lean의 커널에 의해 확인됩니다.
분류가 실제로 말하는 것
유한 단순 그룹은 유한 대칭의 분할할 수 없는 구성 요소이며 "거대한 정리"라는 별명을 가진 분류는 이들의 전체 목록을 제공합니다. 프로젝트 문서에 따르면 모든 유한 단순 그룹은 소수 순서의 순환 그룹, 최소 5개 기호의 교대 그룹, 유한 필드 위에 구성된 Lie 유형 그룹의 16개 무한 패밀리 중 하나, 또는 어떤 패밀리에도 적합하지 않은 정확히 26개의 산발 그룹 중 하나의 네 가지 종류 중 하나입니다.
이 목록에 모든 가능성이 있음을 증명하는 데는 한 세기 동안의 공동 노력이 필요했습니다. 이 분류의 중심이 된 존 톰슨(John Thompson)은 1970년에 필즈상을, 2008년에 아벨상을 받았습니다. 증명은 너무 길어서 여러 논문과 여러 세대의 수학자에게 배포되었기 때문에 그 완전성에 대한 의문이 수십 년 동안 지속되었습니다. 이러한 공식화에 대한 의심은 이제 공식적으로 해소됩니다.
500개 소스에 걸친 수많은 에이전트
원본 증거는 500개 이상의 기사와 책에 흩어져 있으며, 그 중 다수는 수십 년 전에 호환되지 않는 표기법으로 작성되었습니다. Axiom 엔지니어는 Hacker News 릴리스 토론에서 이 방법을 설명했습니다. 에이전트 떼가 이러한 모든 소스를 검토하는 임무를 맡았으며, 동일한 비공식 개념이 약간 다르지만 수학적으로 호환되지 않는 방식으로 형식화될 수 있기 때문에 모든 것을 일관된 전체로 조립하는 것이 어려운 부분이었습니다.
회사의 블로그 게시물에 따르면 작업이 시작부터 출시까지 24일이 걸렸으며 인간 엔지니어와 수학자들이 한 줄씩 작업하는 대신 에이전트 무리를 조종했습니다. 이 결과는 프론티어 모델을 사용하여 생성된 주요 고전 정리의 린 증명을 포함하여 2026년에 주목받는 자동 형식화 이정표를 따르는 것이지만 이전 프로젝트에서는 접근하지 못한 규모입니다.
34 공개된 기록과의 차이
출판된 증명을 기계가 확인할 수 있는 형태로 번역하면 수학 문헌의 실제 문제가 노출됩니다. Axiom은 대부분의 문제가 인쇄상의 오류, 표의 실수, 가설 삭제 등 사소한 문제라고 보고합니다. 그러나 공식화가 진행되기 전에 해결해야 할 출판된 기록과의 34가지 주목할 만한 편차가 있었습니다.
가장 중요한 것은 불균형 그룹 정리(Unbalanced Group Theorem)에 관한 것입니다. 결과에 대한 1세대 경로를 공식화하는 동안 팀은 발표된 주장에 사용된 종결 주장에 대한 반례를 발견했습니다. 전문가 그룹 이론가들과의 협의를 통해 그들은 Daniel Gorenstein 시대의 구조 기술, 특히 1970년대의 최대 2성분 이론을 기반으로 구축된 대체 경로를 구축하고 그 수정 사항을 새로운 35페이지 그룹 이론 논문으로 발표했으며 사전 인쇄 번호 2610.00575로 게시되었습니다. 이 회사는 수학계의 이익을 위해 해당 분류 작업의 기반이 되는 그룹 이론가들과 협의하여 작성된 긴 정오표 목록을 공개할 것이라고 밝혔습니다.
기계 검증 수학이 중요한 이유
형식화의 가치는 컴퓨터가 증명을 승인했다는 것만이 아닙니다. 린 형식화는 흩어져 있는 전문가들이 수천 페이지를 읽어 축적된 신뢰를 얻는 대신, 작고 철저하게 감사되는 프로그램인 증명 보조자의 커널에 대한 신뢰 기반을 줄입니다. 이 이야기가 수백 개의 찬성표를 얻은 Hacker News 스레드의 논평자들은 분류가 유지되는 이유에 대한 경험적 지식이 원래 세대의 수학자들이 은퇴함에 따라 말 그대로 사라질 위험에 처해 있다고 지적했습니다. 그 이유는 한 사람도 전체 주장을 머리 속에 담을 수 없기 때문입니다.
물리학의 다른 곳에서도 실용적인 반향이 있습니다. 26개의 산발성 그룹 중 가장 큰 괴물 그룹은 유한 대칭을 모듈식 기능과 연결하는 "괴물 같은 달빛" 프로그램(1998년 Richard Borcherds가 필즈 메달을 받은 작업)과 괴물의 대칭을 단순화된 3차원 우주의 블랙홀 엔트로피와 연결하는 Edward Witten의 2007년 제안에 나타납니다. 검증된 분류는 바로 이러한 종류의 학제간 응용을 위해 기본 구조 수학을 더욱 확고한 기반으로 삼습니다.
다음에 나올 내용
Axiom은 정오표 프로젝트와 함께 공식화에서 파생된 더 많은 논문이 진행 중이라고 말합니다. 공식 방법 커뮤니티의 경우 이번 릴리스는 상담원 주도 검증 프로젝트가 시도할 수 있는 새로운 벤치마크를 설정합니다. 수학의 경우, 반세기에 걸친 광범위한 공동 성과를 모든 컴퓨터에서 확인할 수 있는 단일 결과물로 변환합니다. 분류는 더 이상 단순히 믿어지지 않습니다. 이제 가장 문자 그대로 입증되었으며, 누구든지 다운로드하여 확인할 수 있습니다.
