수학 증명의 형식화, AI 자동화 시대 열리다

핵심 요약

• 형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다.
• 증명 보조기(proof assistant) 중 Lean이 수학자들에게 가장 인기 있으며, 2013년 Leo de Moura가 개발했고 마이크로소프트에서 오픈소스로 공개됐다.
• Lean의 표준 수학 라이브러리인 mathlib은 약 30만 개 정리, 10만 개 이상 정의, 250만 줄 코드로 700명 이상이 기여했다.
• 자동 형식화(autoformalization)는 2026년 현실화됐으며, 2025년 말부터 AI가 논문 PDF를 읽어 Lean 형식 증명으로 출력하기 시작했다.
• 2026년 주요 성과: 9월 Anthropic이 페르마 최종 정리를 1천3백만 줄 Lean 코드로 11일 만에 자동 형식화했고, OpenAI는 Navier-Stokes 정리를, Meta는 26개 교과서 대부분을 ATLAS 프로젝트로 자동 형식화했다.
• Lean은 타입 이론(type theory)을 기반으로 하며 CIC(Calculus of Inductive Constructions) 방언을 사용하는데, 타입을 서로 교집합 없는 집합처럼 취급한다.
• Lean 4는 2023년 9월 출시 전 2개, 2025년 5월 1개 사운드니스 버그가 발견·수정됐으나, 2026년 여름 '사운드니스 버그의 여름'에 다수의 심각한 버그가 발견됐고 모두 신속히 수정됐다.
• Ramana Kumar와 Dan Selsam(OpenAI) 같은 보안 연구자들이 frontier 모델 AI로 버그를 발견했으며, Selsam의 사이버보안 전문 AI는 추가 결함을 찾을 수 없을 때까지 협력했다.
• Joachim Breitner는 2026년 9월 Con-Leche라는 검증된 Lean 커널을 공개했으며, Lean으로 구현되고 Claude가 코드와 증명을 생성했으며 ZF 집합론 기반으로 consistency를 형식화했다.
• Con-Leche의 consistency 증명은 10여 개 이상의 다른 증명 검사기로 검증됐으며, 컴파일러·런타임·컴퓨터 환경에 대한 가정을 포함한다.
• Mario Carneiro의 박사 논문(2019)은 Lean 타입 이론 기초이나 오류가 발견됐고 Lean 3 기준으로 오래됐으며, 정의적 동등성이 결정 불가능함을 증명했다.
• 고유 타입화(unique typing) 같은 기본적 성질과 set theory 상대적 consistency를 포함한 여러 기초 질문이 여전히 미해결되어 있으며, 50% 이상의 메타이론 연구가 AI 자동화에 의존하는 것에 대한 우려가 제기됐다.
• Ken Thompson의 '신뢰에 관한 성찰'을 상기하며, 2026년 여름 AI의 버그 수정 과정에서 악의적 백도어가 심어졌을 가능성과 중요 인프라 보호 소프트웨어로 악용될 위험을 경고했다.