AI BriefingAxiom Math, Lean으로 유한 단순 군 분류(CFSG) 첫 컴퓨터 검증 증명 완료
·2026.10.28 09:00
핵심 내용
Axiom Math가 Lean으로 CFSG 증명을 검증하며 기존 문헌의 34개 오류를 발견했다
자세히 보기
- Axiom Math가 2026년 10월 Lean 증명 어시스턴트에서 유한 단순 군 분류(CFSG)의 첫 번째 세대 증명을 형식화하여, 컴퓨터 검증 증명의 완료를 발표함
- AI 에이전트 스웜을 24일간 활용하여 약 4,310만 줄의 코드를 생성하고, 2026년 10월 2일부터 25일까지 108개의 마일스톤을 달성함
- 형식화 과정에서 기존 문헌과 일치하지 않는 34개의 중대한 편차를 발견했으며, 이는 PSL₂(49)와 PSL₂(7)를 포함하는 John Walter의 비대칭 군 정리(UGT) 증명 내 폐쇄 명제의 반례를 포함함
- UGT의 공백을 해결하기 위해 새로운 보존 정리(Theorem 2.3)를 개발 및 형식화했으며, 이후 해당 정리를 우회하는 첫 세대 방법 내의 단축 경로를 발견함
- 증명은 Mathlib를 기반으로 Qiuzhen-CFSG 프로젝트의 120만 줄 코드를 포함하며, 군론 커뮤니티를 위한 정정 목록을 제공함
- 외부 자문위원 Richard Lyons와 Ronald Solomon이 UGT 문제 해결 및 정정 목록 큐레이션에 기여함
이 한국어 요약은 AI가 자동으로 만들었습니다. 원문의 주장과 맥락은 원문에서 확인해 주세요. 저작권은 원저작자에게 있습니다.
