수학자가 Lean 정리 증명기에 대해 알아야 할 것: 신뢰성과 AI

AI가 수학 논문을 형식 증명으로 바꾸는 자동 형식화가 실용화됐지만, Lean 증명을 받아들이려면 커널 검증과 인간의 명제 충실성 감사가 모두 필요함 2026년 여름 AI를 활용한 보안 연구자들이 Lean에서 거짓 명제도 증명할 수 있는 건전성 버그를 여러 개 발견했으며, 모두 수정한 뒤 mathlib를 다시 검증함 신뢰성을 높이는 방안은 독립 커널 간 교차 검증, 커널 자체의 형식 검증, Lean 타입 이론의 기초 연구 강화이며, 어느 접근에도 가정과 한계가 있음 검증된 커널 Con-Leche는 집합론에 상대적인 무모순성 증명을 제공하고 mathlib를 검사했지만, 이는 Lean의 추상 타입 이론 전체에 대한 무모순성 증명과 기술적으로 다름 타입의 유일성 등 기본 성질도 아직 증명되지 않았으며, 수학의 기초를 AI에 맡기려면 인간이 이해할 수 있는 이론적 해설과 면밀한 감사가 필요함 형식 증명과 Lean의 수학 라이브러리 형식 증명은 수학의 기초와 기본 논리 규칙 수준에서 모든 단계를 검사한 증명으로, 단계가 너무 많아 일반적으로 전용 소프트웨어로 검증함 형식화된 결과에는 4색 정리, Feit-Thompson 홀수 위수 정리, Kepler 추측, 구면 뒤집기, 8차원과 24차원 구 채우기, 외력이 있는 Navier-Stokes 해의 폭발, Fermat의 마지막 정리가 있음 이 중 8차원과 24차원 구 채우기, 외력이 있는 Navier-Stokes 폭발, Fermat의 마지막 정리 형식화는 2026년에 완료됨 증명 보조기, 정리 증명기, 대화형 정리 증명기는 여기서 같은 뜻으로 사용함 Automath, HOL Light, Isabelle, Coq, Metamath, Mizar, Lean 등이 있으며, Coq는 2025년 Rocq로 이름을 바꿈 Freek Wiedijk가 편집한 『The Seventeen Provers of the World』는 여러 증명기에서 √2의 무리수성을 증명하며 시스템을 비교함 Lean은 Leo de Moura가 Microsoft 재직 중인 2013년 개발해 공개했으며, Microsoft를 설득해 오픈소스로 배포함 Kevin Hartnett의 『The Proof in the Code』에 따르면 첫 사용자는 Jeremy Avigad였으며, 그는 2015년 Lean 세미나를 운영함 수학자 사이에서는 Lean이 가장 인기 있는 정리 증명기임 mathlib는 Mario Carneiro와 Joha...