수학자 100명이 수십년 걸린 수천 쪽짜리 증명, 컴퓨터로 전부 검증 완료됨 (오류도 잡아냄)

요약 수학계의 거대한 난제이자 수십 년에 걸친 집대성으로 꼽히는 '유한단순군 분류 정리(Classification of Finite Simple Groups, CFSG)'가 정리 증명 보조 프로그램인 린(Lean)을 통해 마침내 컴퓨터 검증(포멀라이제이션)을 마쳤습니다. 유한단순군 분류 정리는 모든 유한단순군이 소수 위수의 순환군, 교대군, 리 형태의 군, 혹은 26개의 산재군(sporadic groups) 중 하나임을 밝혀낸 정리로, 1세대 증명만 해도 약 100여 명의 수학자가 참여해 수천 페이지 분량의 논문을 발표해야 했던 수학 역사상 최대 규모의 공동 프로젝트 중 하나입니다. 이번 프로젝트팀은 이 1세대 증명을 바탕으로 린(Lean)의 커널이 모든 논리적 단계를 완전히 검증할 수 있도록 코드화했습니다. 이번 포멀라이제이션 작업 과정에서는 놀라운 성과도 함께 나왔습니다. 과거 발표되었던 논문 중 '불균형 군 정리(Unbalanced Group Theorem)' 증명에 사용된 한 폐포(closure) 단언에서 반례를 발견한 것입니다. 연구팀은 기존 논문의 논리적 결함을 확인한 뒤, 1976년 솔로몬(Solomon)의 극대 2-성분 이론을 기반으로 단순군 케이스에 대한 대체 논리를 새로 구축해 증명을 완결 지었습니다. 공개된 통계에 따르면 이번 프로젝트에는 무려 4,310만 라인의 린 코드, 205만 개 이상의 선언, 715권에 달하는 논문 및 서적이 투입되었습니다. 연구진은 현재 군론 학자들과 협력하여 기존 문헌에서 발견된 오류 목록(errata)을 정리하고 있으며, 향후 이를 모두 공개할 예정입니다.