유한 단순군 분류 정리의 Lean 형식화: Axiom의 AI 에이전트 증명이 확인하는 것

Axiom Math는 유한 단순군의 분류(classification of finite simple groups, CFSG)에 대해 "최초의 완전한 컴퓨터 검증 증명"을 만들었다고 말합니다. 이 정리의 증명은 흔히 수학에서 가장 긴 증명으로 불립니다. Axiom의 연구 글¹에 따르면 엔지니어와 수학자들은 24일 동안 "수십 개 AI 에이전트로 이루어진 무리(swarm)들을 지휘"했고, 에이전트들은 Lean 코드 약 4,310만 줄을 썼습니다. Lean은 컴퓨터가 증명의 모든 단계를 확인하는 언어입니다. 그 과정에서 에이전트들은 분류의 핵심 결과 가운데 하나에 이르는 1986년 경로의 한 단계에 대한 반례를 찾았고, Axiom은 그 단계를 대신할 새 논증을 공개했습니다. 연구 글의 날짜는 2026년 10월 26일입니다. 코드²와 논문⁵, X 발표는 10월 27일에, 57쪽짜리 정오표 문서⁴는 10월 28일에 나왔습니다.

X 발표는 "인류 역사상 가장 큰 수학 증명이 이제 컴퓨터로 검증되었습니다."라는 문장으로 시작합니다.⁶ 정확한 주장이지만, 들리는 것보다 범위가 좁습니다. Lean은 증명이 형식적 명제와 짧은 공리 목록에서 한 단계씩 따라 나오는지를 확인합니다. 그 형식적 명제가 군론 학자들이 말하는 CFSG를 뜻하는지, Axiom이 공개한 정오표의 96개 항목이 옳은지는 확인하지 않습니다. 또 10월 30일 현재, Axiom 밖의 누군가가 이 검사를 다시 돌렸다는 보고는 찾지 못했습니다. Axiom 스스로도 명제와 빌드에 대한 외부 확인을 청하고, 정오표에 대한 정정을 요청합니다.

아래에서는 이 정리가 무엇을 말하는지, Axiom이 무엇을 공개했는지, Lean 파일이 무엇을 확립하는지, Axiom이 문헌에서 무엇을 찾았는지, 문서마다 수치가 어떻게 다른지, 사람에게 남은 일은 무엇인지 정리합니다. 모든 출처는 2026년 10월 30일에 확인했습니다.

유한 단순군의 분류란 무엇인가요?#

군은 결합할 수 있고 되돌릴 수 있는 대칭들의 모음입니다. Axiom의 글은 정육면체를 예로 듭니다. 24가지 회전은 정육면체를 똑같아 보이게 두고, 그중 두 회전을 잇달아 하면 24가지 가운데 또 하나가 되며, 각 회전은 되돌릴 수 있습니다.¹ 자연수가 소수로 분해되듯, 유한군은 더는 쪼갤 수 없는 조각들로 분해됩니다. 그 조각이 유한 단순군입니다.

CFSG는 그 조각을 모두 나열합니다. Axiom 자체 논문의 표현으로는 "모든 유한 단순군은 소수 위수의 순환군이거나, n ≥ 5인 교대군 A_n이거나, 리 형(Lie type) 단순군이거나, 스물여섯 개 산재군(sporadic group) 가운데 하나다".⁵ 가장 큰 산재군인 괴물군(Monster)의 원소는 약 8 × 10^53개입니다.

어려운 것은 증명입니다. Axiom의 글은 이 증명을 "약 100명의 수학자가 쓴 500편이 넘는 논문, 대략 1만 5,000쪽"이라고 묘사합니다. Daniel Gorenstein은 1983년 분류가 완성되었다고 발표했지만, 한 경우인 준얇은 군(quasithin group)은 Michael Aschbacher와 Stephen Smith가 2004년 1,221쪽 분량의 논의를 출판할 때까지 열려 있었습니다. Gorenstein, Richard Lyons, Ronald Solomon, 그리고 나중에 합류한 Inna Capdeboscq의 2세대 증명은 지금도 출간되고 있습니다. 글은 2023년까지 열 권이 나왔다고 세고, 적어도 열두 권이 될 것으로 봅니다. Axiom의 발표 스레드는 문제를 이렇게 표현합니다. "누구도 전체를 읽지 않았습니다. 너무 크니까요."⁶

Axiom은 무엇을 발표했나요?#

Axiom은 10월 1일 프로젝트를 조율할 Slack 채널을 열었고, 첫 에이전트 '무리'는 10월 2일 가동되었습니다.¹ 기존 Lean 작업과 문헌에서 모은 증명 지도가 프로젝트를 108개 마일스톤과 약 380개의 작은 과제로 나눴습니다. "선임 에이전트들이 어려운 논증을 분해하고 형식화되는 명제를 검토했으며", 다른 에이전트들은 기존 결과를 찾거나 Lean 증명을 썼습니다. 10월 10일 채널에는 "우리가 괴물군이 단순군임을 증명했다."라는 글이 올라왔습니다. 모든 것이 앞으로만 나아가지는 않았습니다. 일부 마일스톤은 에이전트들이 "증명하지 않고 가정한" 전제 조건 위에 서 있는 것으로 드러났고, "그 가정 위에 쌓은 수만 줄을 지웠습니다".

AI 쪽에 대해 글은 "에이전트들은 계속 바뀌는 여러 모델을 섞어 썼고, 조율 도구가 그 작업을 뒷받침했다"고만 말합니다. 모델 이름은 하나도 밝히지 않습니다. 사람 쪽에 대해서는 "인간 수학자들은 수학적 장애물을 조사했고, 엔지니어들은 커져 가는 시스템이 계속 생산적으로 돌아가게 했다"고 씁니다. 프로젝트 사이트는 기여자 31명을 올리고, 그중 4명을 핵심 기여자로 표시합니다.³

형식화는 Lean의 주요 수학 라이브러리인 Mathlib과, 아래에서 설명할 두 번째 라이브러리 Tau Ceti 위에 세워졌습니다. 글에 따르면 Qiuzhen-CFSG에서 가져온 약 120만 줄도 들어 있습니다. Qiuzhen-CFSG는 앞서 진행된 공개 프로젝트로, README에는 Feit–Thompson 정리, Bender–Suzuki 정리, Gorenstein–Walter 정리가 완료된 것으로 적혀 있습니다.¹⁴

공개는 여러 조각으로 나뉘어 이루어졌습니다.

조각	날짜	내용
연구 글1 "Formalizing the Enormous Theorem"	10월 26일 자	진행 경위, 수치, 문헌에서 찾은 문제
X 스레드6, @axiommathai	10월 27일 14:34 UTC	발표와 확인 요청
GitHub 저장소2 AxiomMath/CFSG	10월 27일, 커밋 1개(15:07 UTC)	Lean 코드, Apache-2.0 라이선스
The Unbalanced Group Theorem5, Hexagon 2610.00575v1	10월 27일	새 논증을 담은 35쪽 논문
Selected Departures from Published Arguments4	10월 28일	정오표: 57쪽, 96개 항목

Lean 파일은 실제로 무엇을 확립하나요?#

명제, 그리고 그 출처

저장소의 대표 정리인 Comparator/Solution.lean의 CFSGComparator.classification은 TauCeti.ClassificationStatement를 증명합니다. README²는 그 명제를 이렇게 인용합니다.

def ClassificationStatement : Prop :=
  ∀ (G : Type u) [Group G] [Finite G] [IsSimpleGroup G],
    ∃ i : CFSGIndex, Nonempty (G ≃* i.Group)

말로 풀면, 모든 유한 단순군 G에 대해 목록에 어떤 항목 i가 있어서 G가 그 항목이 정의하는 군과 동형이라는 뜻입니다. 목록 CFSGIndex에는 네 종류의 항목이 있습니다. 소수 위수의 순환군, 다섯 개 이상의 문자 위의 교대군, 명시적인 대수적 데이터로 만든 리 형 군, 그리고 각각 유한 표시(생성원과 그 사이의 관계)로 주어진 26개 산재군입니다.

이 명제는 Axiom이 쓴 것이 아닙니다. 출처는 Tau Ceti¹¹로, "Lean FRO와 Mathlib Initiative가 인큐베이팅한" Lean 라이브러리이며, 이곳에서는 "로드맵은 사람이 맡고" "코드는 AI가 맡습니다". Tau Ceti의 이 명제 로드맵은 2026년 8월 8일에 추가되었고,¹³ 명제 자체는 9월 25일에 병합되었습니다.¹² Axiom의 저장소는 Tau Ceti를 10월 2일의 커밋에 고정합니다. 즉 이 명제는 다른 프로젝트를 위해 쓰였고, 10월 1일 Axiom의 프로젝트가 시작되기 전에 이미 공개되어 있었습니다.

이 명제는 한 방향만 말합니다. 모든 유한 단순군이 목록에 있다는 것입니다. Tau Ceti 파일¹²은 무엇을 빼놓았는지 분명히 밝힙니다. "여기서는 목록에 오른 밑집합(carrier)의 유한성이나 단순성을 주장하지 않는다". Tau Ceti 로드맵은 목록에 오른 군의 "유한성, 단순성, 위수"를 "후속 작업"으로 남겨 둡니다. Axiom의 저장소는 Axiom 자체의 정의로 두 번째, 더 넓은 정리도 증명하는데, 여기에는 목록의 군들이 유한하고 단순하다는 내용이 더해집니다.² 이 정리를 읽으려면 Axiom의 정의도 함께 읽어야 합니다.

공리, 그리고 native_decide 없음

README는 증명이 "표준 공리 Classical.choice, propext, Quot.sound(native_decide 없음)"를 쓴다고 말합니다. 각각 선택 공리, 명제 외연성, 몫의 건전성입니다. Lean은 어떤 정리가 기대는 공리를 모두 나열할 수 있으므로, 숨은 가정이 더 있다면 드러납니다.

native_decide는 큰 계산을 위한 지름길입니다. Lean 레퍼런스¹⁶는 이것이 "Lean 컴파일러 전체를 신뢰해야 하는 부분에 더하며, #print axioms에 새 공리가 나타난다"고 경고합니다. 이것을 피하면 신뢰해야 하는 부분이 모든 증명을 확인하는 Lean 커널과 세 공리로 한정됩니다. Axiom은 비용이 큰 유한 계산을 "따로 확인할 수 있는 인증서"로 옮겼다고 말합니다. 직접 열어 본 인증서 파일은 decide +kernel을 쓰는데, 이는 커널이 계산을 직접 하게 합니다.

sorry 없음, 그리고 Lean 버전

Lean에서 sorry는 "완성되지 않은 전술 증명을 위한 임시 자리 표시자"입니다.¹⁶ sorry가 있는 파일도 경고와 함께 컴파일되며, 그것에 기대는 모든 정리에는 공리 sorryAx가 붙습니다. 'sorry 없음(sorry-free)'은 자리 표시자로 남겨 둔 단계가 없다는 뜻이고, 위의 공리 목록이 그 확인입니다. 목록에 sorryAx가 없습니다. 저장소의 메타데이터 파일에는 sorry_count: 0이 기록되어 있습니다.

의도적인 sorry는 하나뿐이며, 증명 없이 목표 명제만 적어 둔 Comparator/Challenge.lean에 있습니다. 설정 파일은 Lean의 comparator 도구에게, 해답이 정확히 그 명제를 허용된 세 공리만으로 증명하는지, 그리고 커널이 그것을 받아들이는지 확인하게 합니다. 도구의 README¹⁵에 따르면 Lean 4.35.0부터 이 검사는 lake comparator로 Lean에 포함되어 배포됩니다.

프로젝트는 릴리스 후보인 Lean v4.35.0-rc3으로 빌드되며, Mathlib과 Tau Ceti를 정확한 커밋에 고정합니다. 그래서 다시 빌드할 때 같은 도구 체인, 라이브러리, 명제를 쓸 수 있습니다.

같은 메타데이터 파일은 작업이 어떻게 검토되었는지도 적고 있습니다. status: self-assessed와 reviewers: ["Axiom Math"], 그리고 자동화 항목은 method: autonomous, framework: "AxiomProver"입니다.

Lean 커널이 확인하는 것	사람이 여전히 확인해야 하는 것
최종 정리에서 세 공리까지 거슬러 올라가는 모든 추론	ClassificationStatement와 그 목록의 정의들이 CFSG를 뜻하는지
sorry로 남겨 둔 단계가 없다는 것	공개된 파일로 다른 사람의 컴퓨터에서도 빌드가 성공하는지
인증서 파일 속 유한 계산	정오표 96개 항목이 각각 옳은지, 그리고 새로운 것인지
	형식화가 역사적 증명을 한 단계씩 따르는지

마지막 행에 대해서는 글 스스로 이렇게 말합니다. "형식적 전개가 특정한 역사적 논증의 각 단계를 재현하는지는 별개의 질문이다".¹

Axiom은 문헌에서 무엇을 찾았나요?#

에이전트들은 작업하면서 의심되는 문제를 기록했습니다. 글은 그 대부분이 "무해한 것으로 드러났다. 오타, 표의 오류, 빠진 가정, 또는 맥락에서 분명한 단계들이었다. 몇 가지는 진짜 수학이 필요했다"고 말합니다.¹ Aschbacher와 Smith의 준얇은 군 책에 있는 한 보조정리에서는 군 SL₂(5)에 대해 "주장된 등식에는 2가 필요한 곳에서 한 양이 1이었다".

비균형군 정리

가장 큰 사례는 비균형군 정리(Unbalanced Group Theorem, UGT)에 관한 것입니다. Axiom의 논문은 이 정리를 이렇게 요약합니다. 분류의 귀납 가정 아래에서 "대합의 중심화군에서 정규인, 홀수 위수의 자명하지 않은 부분군이 있으면, 그것을 품은 단순군은 홀수 표수의 리 형 군이거나 특정 차수의 교대군일 수밖에 없다".⁵ 대합(involution)은 위수가 2인 원소입니다. 논문의 표현으로는 "따라서 UGT는 남은 분류 문제에서 비균형군을 모두 없앤다".

Axiom은 1세대 증명을 따르기로 했기 때문에, UGT에 이르는 출판된 경로 가운데 하나인 John Walter의 1986년 장편 논문(memoir)을 하나하나 짚어 갔습니다. Walter는 q가 홀수이고 9와 페르마 소수, 메르센 소수를 제외한 군들의 족 PSL₂(q)를 정의합니다. 그의 논증은 어떤 연산, 즉 대합의 중심화군(centralizer)의 성분(component)을 취하는 연산을 해도 그 족 안에 머문다고 주장합니다. 에이전트들은 대합이 체 자기동형사상(field automorphism)일 때는 그렇지 않다는 것을 찾아냈습니다.

Walter의 족에 속한 군	중심화군의 성분	족 밖에 있는 이유
PSL₂(49)	PSL₂(7)	7은 메르센 소수
PSL₂(81)	PSL₂(9)	9는 명시적으로 제외됨
PSL₂(289)	PSL₂(17)	17은 페르마 소수

논문은 범위를 신중하게 다룹니다. "즉 우리는 이 추론의 빈틈을 확인한 것이지, 그 명제 자체나 UGT에 대한 반례를 찾은 것이 아니다." 또 "이 어려움은 CFSG에 걸림돌이 되지 않는다"고 하며, UGT에 이르는 다른 경로를 듭니다. Morton Harris의 논증을 따른 Gorenstein의 1983년 책의 설명, 그리고 Gorenstein, Lyons, Solomon의 2세대 작업에서 이끌어 내는 방법입니다.

Hexagon에 올라온 새 논증

Axiom에게는 자신이 쌓고 있던 1세대 증명에 맞는 대체 논증이 필요했습니다. 그 결과가 표제 면에 "Axiom Math"라고 적힌 35쪽 논문 The Unbalanced Group Theorem⁵입니다. 이 논문은 10월 27일 수학 연구 저장소 Hexagon에 올라왔습니다. Hexagon은 기여자로 Colin Defant와 Ken Ono를 표시하는데, 두 사람 모두 Axiom의 수학 기여자 명단에 있습니다. 또 선언 두 가지를 보여 줍니다. "주로 사람이 쓴 텍스트"와 "사람의 이해: 모든 부분"입니다.

주결과는 정리 2.3 "단순 상층(simple top)의 보존"입니다. Axiom의 글은 이것을 "AxiomProver가 증명한 군론의 새로운 결과"라고 부릅니다. 논문은 비고 9.5에서, 같은 환원을 쓰면 정리 2.3 없이도 UGT를 더 짧게 이끌어 낼 수 있다는 점도 기록합니다. 글에 따르면 Axiom의 수학자들은 형식화 이후에 이 지름길을 찾았습니다. 논문은 "AxiomProver가 이 경로를 형식화했기 때문에" 더 긴 논증을 그대로 둡니다.

Lyons와 Solomon의 역할

Lyons와 Solomon은 둘 다 원래의 분류 작업에 참여했습니다. Axiom의 글에 따르면 두 사람은 논증에 대해 자문했고, UGT 수정은 "Lyons, Solomon과 주고받은 서신의 도움을 받았다". 글은 또 이렇게 말합니다. "Lyons는 가능한 증명 경로를 명확히 하고 이 장애물을 역사적 맥락 속에 자리매김하는 데 도움을 주었다. Solomon의 1976년 극대 2-성분 이론은 AxiomProver가 만들고 형식화한 대안 논증의 핵심 아이디어를 제공했다." 논문은 사사에서 Lyons, Dan Nakano, Solomon에게 감사를 표하며, Axiom은 "Richard Lyons와 Ronald Solomon을 포함한 군론 학자 자문단"과 함께 정오표를 계속 관리하겠다고 말합니다.

이 설명들은 Axiom의 것입니다. 형식화에 대해 Lyons나 Solomon이 공개적으로 밝힌 입장은 찾지 못했습니다.

Axiom은 정정을 몇 건이라고 보고했나요?#

문서마다 수치가 다릅니다.

출처	날짜	내용
연구 글1	10월 26일 자	"해결해야 했던, 출판된 기록과의 주목할 만한 차이 34건". 문제 대부분은 "사소한" 것
@axiommathai 스레드6	10월 27일	"중대한 정오 사항 수백 건도 바로잡았습니다. 추후 공개 예정."
@andrew_v102097, 공개를 알리며("오늘 아침 저희가 공개합니다")	10월 27일	"문헌에 대한 실질적 수정 100건"
정오표 문서4	10월 28일	96개 항목: A부 34개, B부 62개

코드 규모도 다릅니다. 글과 프로젝트 사이트는 Lean 4,310만 줄이라고 하고,^1,3 X 스레드는 "Lean 5,000만 줄"이라고 합니다.⁶

무엇을 세었는지 밝히는 것은 정오표 문서뿐입니다. 첫 쪽에는 이렇게 적혀 있습니다. "96개 항목은 선별한 수학적 이탈과 보충 설명을 기록한 것이다. 96개의 오류나 새로운 발견을 집계한 것이 아니다. 이것은 포괄적인 정오표가 아니다."⁴ 일상적인 조판 수정과 표기 변경, 그리고 "쉽게 고칠 수 있는 실수는 생략했다". A부에는 "구조적 변경과 대안 증명"에 관한 항목 34개가 있는데, 연구 글의 집계와 같은 수입니다. B부에는 "추가 논증과 국소적 수정"에 관한 항목 62개가 있습니다. 문서는 이 분류가 "오류의 정도나 수학적 중요도의 척도가 아니라, 논증이 바뀐 정도를 나타낸다"고 말합니다.

정오표는 어떻게 만들어졌는지도 밝힙니다. "이 문서는 AI 시스템 AxiomProver가 생성했다." 그리고 "AxiomProver가 여기 기술된 모든 수정, 보충 논증, 대안 증명을 자율적으로 만들었다"고 덧붙이며, "일부 수정은 이미 알려져 있었고, 그것을 포함한 것이 우선권을 주장하는 것은 아니다"라고 씁니다.

아직 사람이 해야 할 일은 무엇인가요?#

명제 읽기

Axiom의 글은 일을 이렇게 나눕니다. "사람은 그 명제와 명제가 쓰는 정의를 살펴 그것이 의도한 분류를 표현하는지 확인하고, Lean은 그것을 확립하는 형식적 연역을 확인한다."¹ Axiom은 X에서 바로 그 일을 요청했습니다. "군론 학자들과 Lean 커뮤니티가 이를 검증해 주시기를 청합니다. 증명 검사를 다시 돌리고, Lean 명제가 CFSG가 말하는 것을 말하는지 확인해 주십시오."⁶

이것이 중요한 이유는 이렇습니다. 이런 형태의 명제는 그 목록만큼만 좋습니다. 목록의 정의 하나가 의도한 것과 다른 군을 기술한다면 정리는 CFSG가 아닌 다른 것을 말하게 되고, 그래도 Lean은 증명을 받아들일 것입니다. Tau Ceti의 로드맵¹³도 자신의 정의에 대해 같은 말을 합니다. "이 요구 사항은 기계적으로가 아니라 검토를 통해 지켜진다". 로드맵은 Lean의 공리 검사가 "정직한 구성과, 목표 존재 정리에서 밑집합을 골라 오는 구성을 구별할 수 없다"고 설명하며, 그래서 "각 작업 항목의 검토자는 정의를 읽고 밑집합을 명시적 데이터까지 거슬러 추적해야 한다"고 말합니다. 10월 25일 생성된 Tau Ceti 자체의 상태 페이지¹³는 그 작업의 한 부분을 '부분 완료'로 표시합니다. 리 형 구성을 표준 군 스킴에 대응시키는 작업은 일부 족에 대해서는 끝났지만 다른 족에 대해서는 아직입니다.

다시 빌드하기

README는 명령 하나 lake build와 함께 메모를 남깁니다. "이 프로젝트의 빌드 시간을 24시간 아래로 줄이기 위해, Lake에 대한 아직 병합되지 않은 변경 몇 가지와 곧 상위 저장소에 반영할 최적화 몇 가지를 사용했다."² 뉴스 사이트 RuntimeWire¹⁰가 10월 27일 Axiom 밖의 누군가가 증명을 빌드하고 확인했느냐고 묻자, Axiom의 CEO Carina Hong은 대변인을 통해 이메일로 이렇게 답했습니다. "아직입니다. 외부에서 독립적으로 재현하도록 돕고 장려하기 위해 빌드 산출물을 공개하고 있습니다." 10월 30일까지 외부에서 전체를 다시 빌드했다는 공개 보고는 찾지 못했습니다. 저장소의 이슈와 풀 리퀘스트를 확인하고 웹을 검색했습니다.

정오표와 새 정리 검토하기

정오표 96개 항목은 AI 시스템이 생성했고 수십 년의 문헌을 다룹니다. 각 항목이 옳은지, 더 단순한 수정이 있는지, 이미 알려진 것인지는 군론 학자들이 답할 질문입니다. 정오표는 그 도움을 청합니다. "정정, 이전 논의에 대한 참고문헌, 더 단순한 논증이나 추가적인 수학 연구를 위한 제안을 환영한다."⁴ UGT 논문은 프리프린트입니다. 그 새 정리를 수학으로 읽는 일은 Lean이 그것을 받아들이는 일과 별개입니다.

수학자들은 지금까지 무엇이라고 했나요?#

Timothy Gowers는 10월 27일 X에 이렇게 썼습니다⁸. "CFSG의 증명이 100% 옳은지 불확실했던 역사를 생각하면, 형식화 자체는 끔찍하더라도 대단한 소식인 것 같다. (실제로 끔찍한지는 모르지만, 내 짐작은 그렇다.)"

블로그에 수학에 관한 글을 쓰는 John D. Cook은 10월 28일 이렇게 썼습니다⁹. "UGT, 그리고 그것에 기대는 CFSG는 옳지만, 증명에는 결함이 있었다." 이것은 Axiom의 자료에 대한 논평이지 확인이 아니며, Axiom의 논문은 발견을 더 좁게 표현합니다. 출판된 한 경로에 빈틈이 있고, Walter의 명제의 결론과 UGT 자체는 반박되지 않았다는 것입니다.⁵

이런 결과는 다른 사람이 확인할 수 있도록 어떻게 기록할 수 있을까요?#

확인하는 사람에게 필요한 것의 상당 부분은 이미 공개되어 있습니다. 정확한 도구 체인, 빌드 파일에 고정된 라이브러리 커밋, 프로젝트 밖에서 가져온 명제, comparator 설정, 날짜가 적힌 정오표 문서입니다. 이력은 보기가 더 어렵습니다. 공개 저장소에는 10월 27일에 만든 "Initial commit" 커밋 하나만 있습니다.² 글이 묘사하는 24일간의 작업은 Slack과 GitHub 이슈에서 조율되었지만, 코드와 함께 공개되지 않고 글 속 이야기로만 전해지며, 모델 이름도 밝혀지지 않았습니다.

다른 사람이 확인할 수 있는 기록이라면 다음을 하나로 묶을 것입니다. 정확한 커밋과 도구 체인, 명제와 그것을 가져온 커밋, 사용한 공리, 각 조각이 공개된 날짜, 누가 무엇을 했는지(사람과 AI, 그리고 모델 이름), 누가 무엇을 확인했고 각 확인의 결과가 무엇이었는지입니다. CFSG의 경우 이런 확인은 여러 달에 걸쳐, 서로 다른 사람에게서, 서로 다른 곳에서 나올 수 있습니다.

Papex는 이 가운데 일부를 위해 만들어졌습니다. 가설, 발견, 출판물을 그 뒤에 있는 사람, 도구, 버전과 연결하고, 책임 있는 사람이 서명하고 날짜를 남깁니다. Papex는 증명을 확인하지 않습니다. 그것은 Lean이 하고, 명제는 사람이 확인합니다. CFSG는 미해결 문제가 아니라 정리이므로, Papex의 문제 목록에도, Papex가 미해결 문제에 관한 AI 활용 주장을 모아 두는 페이지(영어)에도 없습니다.

출처#

1. Formalizing the Enormous Theorem (Axiom Math, 2026년 10월 26일 자 연구 글), 2026년 10월 30일 확인 ↩ a b c d e f g h i
2. AxiomMath/CFSG: README, lean-toolchain, lake-manifest.json, comparator.json, formalization.yaml, Comparator/Challenge.lean, Comparator/Solution.lean, Certificates/Certificate1.lean, CFSG/Milestones/CFSG_classification.lean (GitHub, 커밋 69cb972f, 2026년 10월 27일), 2026년 10월 30일 확인 ↩ a b c d e f
3. CFSG in Lean, 프로젝트 사이트(Axiom Math), 2026년 10월 30일 확인 ↩ a b
4. Selected Departures from Published Arguments: Notes on the formalization of the classification of finite simple groups (Axiom Math, 2026년 10월 28일), 정오표 페이지와 PDF, 2026년 10월 30일 확인 ↩ a b c d e
5. The Unbalanced Group Theorem, hexagon:2610.00575v1 (Axiom Math, Colin Defant와 Ken Ono가 기여, 2026년 10월 27일), 2026년 10월 30일 확인 ↩ a b c d e f
6. Axiom(@axiommathai)의 X 발표 스레드, 2026년 10월 27일, Lean 줄 수, 증명의 규모, UGT와 정오표, 확인 요청에 관한 게시물 포함, 2026년 10월 30일 확인 ↩ a b c d e f
7. @andrew_v10209의 X 게시물, 2026년 10월 27일, 2026년 10월 30일 확인 ↩
8. Timothy Gowers(@wtgowers)의 X 게시물, 2026년 10월 27일, 2026년 10월 30일 확인 ↩
9. John D. Cook, The Unbalanced Group Theorem (2026년 10월 28일), 2026년 10월 30일 확인 ↩
10. Emerson Redding, Axiom publishes Lean proof artifacts to support independent reproduction (RuntimeWire, 2026년 10월 27일), 뉴스 보도, Carina Hong의 이메일 답변에 사용, 2026년 10월 30일 확인 ↩
11. Tau Ceti README (GitHub), 2026년 10월 30일 확인 ↩
12. Tau Ceti, 커밋 6e0c6ac의 CFSG/Classification.lean (2026년 10월 2일), 파일 이력과 풀 리퀘스트 #8792(2026년 9월 25일 병합) 포함, 2026년 10월 30일 확인 ↩ a b
13. Tau Ceti 로드맵, CFSGStatement README (2026년 8월 8일 추가)와 STATUS (2026년 10월 25일 생성), 2026년 10월 30일 확인 ↩ a b c
14. Qiuzhen-CFSG README (GitHub), 2026년 10월 30일 확인 ↩
15. leanprover/comparator README (GitHub), 2026년 10월 30일 확인 ↩
16. Tactic Reference: decide, native_decide and sorry (Lean Language Reference), 2026년 10월 30일 확인 ↩ a b