인공지능(AI)이 수학 논문을 형식 증명(formal proof)으로 자동 변환하는 '자동 형식화(autoformalization)' 기술이 2026년을 기점으로 실용화 단계에 접어들었습니다. 이는 과거 수십 년이 걸리던 복잡한 수학 정리의 형식화를 AI가 단 며칠 만에 수백만 줄의 코드로 생성하는 혁신을 가져왔습니다. 그러나 이러한 발전의 이면에는, 가장 널리 사용되는 대화형 정리 증명기(interactive theorem prover) 중 하나인 Lean의 신뢰성 문제가 새롭게 조명되고 있습니다.
Lean은 마이크로소프트(Microsoft)가 개발하고 오픈소스로 공개한 증명 보조기로, 수학자들 사이에서 가장 인기 있는 도구로 자리 잡았습니다. 특히 방대한 수학 라이브러리인 mathlib는 약 30만 개의 정리와 250만 줄의 코드를 포함하며, AI 자동 형식화의 주요 대상이 되고 있습니다. 하지만 2026년 여름, AI를 활용한 보안 연구자들이 Lean 커널에서 '건전성 버그(soundness bug)'를 여러 개 발견했습니다. 이 버그는 거짓 명제조차도 참으로 증명할 수 있게 만드는 치명적인 결함으로, 발견 즉시 수정되고 mathlib 전체가 재검증되는 과정을 거쳤습니다. 이는 AI가 생성한 형식 증명이라 할지라도, 그 기반이 되는 증명 보조기 자체의 무결성이 얼마나 중요한지를 여실히 보여줍니다.
이러한 신뢰성 문제를 해결하기 위해 독립 커널 간 교차 검증, 커널 자체의 형식 검증, 그리고 Lean의 기반이 되는 타입 이론(type theory)에 대한 기초 연구 강화 등 다양한 대책이 논의되고 있습니다. 특히 최근에는 Lean으로 구현된 검사기 'Con-Leche'가 mathlib를 검사하고 상대적 무모순성 증명(relative consistency proof)을 제공하는 성과를 보이기도 했습니다. 하지만 여전히 컴파일러, 런타임, 컴퓨터 환경 등 다양한 가정과 한계가 존재하며, 인간의 면밀한 감사(audit) 없이는 형식 명제가 의도한 수학적 명제와 일치하는지 완전히 확신하기 어렵습니다. AI가 수학의 기초를 다루는 시대에도, 인간의 개입과 비판적 사고는 수학적 진리의 엄밀함을 지키는 데 필수적인 요소로 남을 것입니다.