수학자 토머스 헤일스가 테렌스 타오의 블로그에 기고한 글은 형식 증명(formal proof)이라는, 그동안 일부 전문가의 영역이던 주제가 왜 지금 실무자에게도 의미를 갖게 되었는지를 설명한다. 형식 증명이란 수학의 토대와 논리 규칙 수준까지 빠짐없이 검증된 증명을 말한다. 단계 수가 방대해 사실상 전용 소프트웨어를 쓴 컴퓨터 검증으로 이뤄진다. 사색정리, 페이트-톰프슨(홀수 차수) 정리, 케플러 추측, 구 외전, 8·24차원 구 쌓기 문제, 강제항이 있는 나비에-스토크스 폭발, 그리고 페르마의 마지막 정리가 형식화된 대표 사례다. 이 중 마지막 세 건은 올해 완료되며 형식화의 가능성에 대한 인식을 크게 넓혔다.
이 분야의 소프트웨어는 증명 보조기, 정리 증명기 등으로 불린다. Automath, HOL Light, Isabelle, Coq(지난해 Rocq로 개명), Metamath, Mizar, Lean 등 다양한 시스템이 개발돼 왔다. 그중 수학자들 사이에서 가장 널리 쓰이는 것이 레안이다. 레안은 2013년 마이크로소프트에 있던 레오 데 모우라가 만들었고, 그가 회사를 설득해 오픈소스로 공개한 것이 큰 자산이 됐다. 2017년 마리오 카네이로와 요하네스 횔츨이 시작한 수학 라이브러리 mathlib은 현재 약 30만 개의 정리, 10만 개 이상의 정의, 250만 줄의 코드, 700명이 넘는 기여자를 보유한 거대 저장소로 성장했다. 라이브러리에 담긴 정의와 정리는 모두 새로운 증명의 재료로 재사용된다. 코시-슈바르츠 부등식을 다시 증명할 필요 없이 인용만 하면 되는 식이다.
자동형식화, 2026년의 현실
과거에는 종이 증명을 사람이 손으로 형식 증명으로 옮겼다. 3차원 구 쌓기에 관한 케플러 추측의 형식 증명에만 약 20 인년(人年)의 노동과 50만 줄가량의 스크립트가 들었다. 이 과정을 자동화하려는 오랜 꿈이 '자동형식화'로 실현되고 있다. AI가 논문(PDF나 TeX)을 읽고 레안 같은 증명기용 형식 증명을 출력하는 방식이다. 2026년 들어 이는 실용 단계에 접어들었다. 9월 4일 앤트로픽이 발표한 페르마의 마지막 정리 자동형식화는 11일 만에 1,300만 줄의 레안 코드를 생성했고, 9월 8일 OpenAI의 강제항 나비에-스토크스 폭발 발표에도 레안 형식화가 함께였다. 같은 날 재러드 리히트만은 '알려진 모든 수학을 형식 코드로 옮긴다'는 목표의 MAP(수학 자동형식화 프로젝트)를 출범시켰다.
왜 커널이 전부인가
레안은 집합론이 아니라 CIC(귀납적 구성의 계산법)라는 타입 이론에 기반한다. 1901년 러셀의 역설이 촉발한 토대 위기에 대해, 체르멜로의 집합론 공리와 타입 이론이라는 두 해법이 나왔는데 레안은 후자 계열이다. 집합이 서로 겹치는 벤 다이어그램이라면, 타입은 겹치지 않고 쌓인 벽돌에 가깝다는 것이 헤일스의 비유다. 자연수 2와 실수 e는 서로 다른 타입에 속하며, 둘을 잇는 데는 명시적 변환이 필요하다. 1997년 베르너의 논문은 ZFC 집합론을 CIC로, 또 그 역으로 번역할 수 있음을 보여 집합론에 익숙한 이들을 안심시킨다.
레안에서 증명 스크립트는 '정교화'를 거친 뒤 커널의 검증을 받는다. 수천 줄의 C++로 된 이 커널은 정교하지만 매우 복잡하다. 250만 줄의 mathlib 어딘가에 거짓 증명이 끼어 있다면, 그것을 걸러내지 못한 커널의 책임이다. 그래서 헤일스는 두 가지를 강조한다. 첫째, 레안 증명은 커널 검증 전에는 믿지 말 것. 둘째, 검증된 정리가 정말 우리가 의도한 명제인지, 정의가 올바른지 사람이 직접 감사할 것. 나비에-스토크스라면 레안의 명제가 페퍼먼의 밀레니엄 문제 서술과 일치하는지, 실수체·편미분·측도 개념이 제대로 정의됐는지를 사람이 확인해야 한다는 것이다. 이 작업은 증명 자체를 검증하는 것보다 훨씬 수월하며, 레안의 비교기(comparator) 도구가 허가되지 않은 공리 사용 검사까지 돕는다.
'건전성 버그의 여름'이 남긴 것
가장 치명적인 결함은 커널이 '거짓'을 증명하게 허용하는 건전성 버그다. 거짓이 증명되면 어떤 명제든 증명되기 때문이다. 헤일스 자신도 2003년 당시 가장 신뢰받던 HOL Light에서 1996년 이후 처음 발견된 건전성 버그를 찾아낸 바 있다. 레안 역시 2023년 9월 레안 4 출시 전후와 2025년 5월에 버그가 있었고, 2026년 여름에는 여러 건이 쏟아져 '건전성 버그의 여름'으로 불리게 됐다. 한 버그는 콜라츠 추측을 부당하게 반증했고, 헤일스는 같은 버그가 케플러 추측의 짧은 거짓 증명을 만들어낸 것을 보고 알게 됐다고 한다. 모두 신속히 수정됐고 mathlib은 고쳐진 커널로 재검증됐다.
주목할 점은 이 버그들을 발견한 주체다. 블랙햇 해커가 아니라 신뢰성에 관심을 둔 보안 연구자들이 최신 AI 모델을 활용해 찾아냈다. 콜라츠 버그는 검증된 ML 구현 CakeML의 공동 저자 라마나 쿠마르가, 다른 여러 건은 OpenAI의 댄 셀섬이 사이버보안 특화 AI로 찾아 레안 FRO에 알렸고, 협업은 그 AI가 '더는 문제를 찾을 수 없다'고 보고하면서 끝났다. 결함을 찾는 데 쓰인 바로 그 프런티어 AI가 결함을 메우는 데도 동원된 셈이다. 재발 방지책으로는 서로 다른 커널을 여럿 만들어 교차 검증하는 방안이 거론되는데, 이미 약 25개의 레안 커널이 'Lean Kernel Arena'에 정리돼 있다. 자동형식화의 규모가 1조 줄을 바라보는 시대에, 신뢰의 최후 보루는 결국 이 작은 커널과 사람의 명제 감사라는 것이 이 글의 핵심이다.