현대 수학에서 가장 방대한 성취 중 하나로 꼽히는 '유한 단순군 분류 정리(Classification of Finite Simple Groups)'가 증명 보조 도구 Lean을 통해 완전히 형식화됐다. AxiomMath가 공개한 이 프로젝트는 분류 정리의 이른바 1세대 증명(first-generation proof)을 Lean으로 옮기고, 모든 논리 단계를 Lean 커널이 직접 검증하도록 한 결과물이다. 종이 위의 수식과 논증을 사람이 눈으로 따라가며 신뢰하던 방식에서 벗어나, 기계가 한 줄 한 줄의 추론을 기계적으로 확인했다는 점이 핵심이다.
유한 단순군 분류 정리는 유한군의 '기본 구성 요소'에 해당하는 단순군을 몇 개의 무한 계열과 26개의 산재군(sporadic group)으로 완전히 목록화한 결과다. 이 증명은 수많은 논문에 흩어진 채 오랜 기간에 걸쳐 조립되어 왔고, 전체를 한 사람이 끝까지 검토하기가 사실상 불가능할 만큼 거대하다. 바로 그런 규모 때문에 '증명이 정말 빈틈없이 맞는가'라는 질문이 늘 따라붙었고, 형식화는 이 질문에 기계적 보증을 제공하려는 시도다.
형식화가 드러낸 증명의 공백
이번 작업의 의의는 단순히 기존 증명을 코드로 옮긴 데 그치지 않는다. 연구진은 1세대 증명을 형식화하는 과정에서, 불균형군 정리(Unbalanced Group Theorem)에 이르는 기존의 한 경로에서 사용되던 '닫힘(closure) 주장'에 대한 반례를 발견했다. 즉 출판된 증명 경로가 참이라고 전제하던 어떤 폐쇄성 성질이 실제로는 성립하지 않는 경우가 존재했던 것이다. 이는 사람이 논증을 서술할 때 '자명하다'고 넘어간 지점이 실제로는 자명하지 않았음을 기계적 검증이 포착해낸 전형적인 사례다.
연구진은 문제를 지적하는 데서 멈추지 않고, 그 장애물이 무엇인지 설명한 뒤 단순군의 경우에 대한 대안 논증을 제시했다. 이 대안은 솔로몬(Solomon)이 1976년에 전개한 극대 2-성분(maximal 2-components) 이론 위에 세워졌으며, 그 핵심 단계는 '단순한 꼭대기(simple tops)의 보존'을 다루는 정리 2.3이다. 결과적으로 형식화 프로젝트가 새로운 군론 결과 하나를 부산물로 낳은 셈이다.
실무자에게 주는 함의
이 소식이 수학 바깥의 IT 실무자에게 의미가 있는 이유는, 여기서 쓰인 방법론이 소프트웨어·시스템 검증과 본질적으로 같은 뿌리를 공유하기 때문이다. Lean 같은 증명 보조 도구는 명세와 증명을 형식 언어로 기술하고, 신뢰 기반(trusted base)에 해당하는 작은 커널만 믿으면 그 위의 모든 추론이 자동으로 검증되도록 설계된다. 이는 인증된 컴파일러, 암호 프로토콜 검증, 고신뢰 시스템의 정형 명세 같은 영역에서 이미 쓰이는 접근과 정확히 같은 구조다.
특히 주목할 대목은, 오랫동안 전문가 공동체의 검토를 거친 '권위 있는' 증명에서조차 숨은 공백이 발견됐다는 점이다. 이는 코드 리뷰나 테스트를 아무리 많이 거친 시스템이라도 사람의 눈으로는 놓치는 가정이 남을 수 있음을 시사한다. 기계적 검증은 '모두가 맞다고 믿어 온 전제'를 명시적으로 드러내 강제로 증명하게 만들고, 그 과정에서 암묵적 가정의 오류를 노출시킨다. 안전성이 중요한 영역일수록 형식 검증이 테스트의 보완재가 아니라 필수재로 자리 잡는 흐름과 맞닿아 있다.
한계와 남는 질문
다만 이 성과를 과대평가하지 않는 것도 중요하다. 이번 형식화의 대상은 1세대 증명이며, 이후 정리된 더 간결한 세대의 증명이나 전체 분류 정리의 모든 변형을 포괄하는 것은 아니다. 또한 발견된 반례와 대안 논증은 단순군의 경우에 초점을 맞춘 것으로, 그것이 분류 정리 전체의 타당성을 흔드는 문제라기보다는 특정 증명 경로의 결함을 수정하고 대체 경로를 확보한 성격에 가깝다. 공개된 자료만으로는 전체 형식화의 세부 범위나 검증에 전제된 공리적 토대를 상세히 판단하기 어렵다는 점도 유의해야 한다.
그럼에도 분명한 것은, 인간이 수십 년에 걸쳐 쌓아 올린 거대한 증명을 기계가 끝까지 검증할 수 있는 단계에 수학이 들어섰다는 사실이다. 그리고 그 검증 과정이 단지 기존 지식을 재확인하는 데 그치지 않고, 사람이 놓친 틈을 메우며 새로운 결과를 낳을 수 있다는 점이야말로 이 프로젝트가 보여준 가장 실질적인 교훈이다.