수학자 토머스 헤일스(Thomas Hales)는 린(Lean) 정리 증명기가 수학 증명을 기초 논리 수준에서 검증하며, AI를 이용한 자동 형식화가 2026년 실용 단계에 들어섰다고 설명했다. 헤일스의 테런스 타오(Terence Tao)의 수학 블로그에 10월 10일 게재된 기고다.
린은 수학 증명을 어떻게 검증하나
형식 증명은 수학의 기초와 논리 규칙에 따라 증명 전체를 빠짐없이 확인한 결과물이다. 사람이 직접 검증할 수도 있지만 단계가 많아 대개 컴퓨터 소프트웨어인 증명 보조기나 정리 증명기를 이용한다. 헤일스는 수학자들 사이에서 린이 가장 널리 쓰이는 증명 보조기라고 소개했다.
린은 2013년 마이크로소프트(Microsoft)에서 레오 데 모라(Leo de Moura)가 개발해 공개했고, 오픈소스로 제공됐다. 2017년에는 린의 수학 라이브러리인 매스립(mathlib) 개발이 시작됐다. 이 라이브러리에는 정리 약 30만개, 정의 10만개 이상과 코드 250만 줄이 들어 있으며, 기여자는 700명을 넘는다. 기존에 증명된 코시-슈바르츠 부등식 같은 결과를 새 증명에서 다시 증명하지 않고 가져다 쓸 수 있다.
AI 자동 형식화, 대규모 증명으로 확산
과거에는 논문 속 수학 증명을 사람이 형식 언어로 옮겨야 했다. 3차원 구 포장 문제인 케플러 추측을 형식화하는 데는 약 20인년이 들었고, 증명 스크립트는 약 50만 줄에 달했다. 자동 형식화는 AI가 논문 파일을 읽고 린 등 증명 보조기에서 검증 가능한 형식 증명을 출력하는 과정이다.
헤일스는 2025년 9월 소수정리의 준자동 형식화부터 2026년의 대규모 작업까지 진행 상황을 소개했다. 2026년 3월 매스(Math Inc.)는 24차원 구 포장 문제를 형식화해 약 50만 줄의 코드를 만들었으며, 코드 정리 뒤 약 20만 줄로 줄였다고 발표했다. 메타(Meta) 연구진은 수학 교재 26권의 상당 부분을 자동 형식화했다. 앤트로픽(Anthropic)이 9월 4일 발표한 페르마의 마지막 정리 작업은 11일 동안 린 코드 1300만 줄을 생성했고, 오픈AI(OpenAI)는 9월 8일 강제력이 있는 나비에-스토크스 방정식의 폭발 정리 발표와 함께 린 형식화를 공개했다.
헤일스는 자동 형식화가 린 외의 증명 보조기와 여러 대규모 언어 모델을 활용해 이뤄졌다고 설명했다. 2026년 1월에는 얀 우르반(Jan Urban)이 위상수학 교재의 상당 부분을 2주 동안 형식화한 13만 줄 규모의 작업을 공개했다. 2025년 9월 매스의 소수정리 준자동 형식화는 AI가 막힐 때마다 사람이 추가 지침을 줘야 했기 때문에 ‘준자동’에 그쳤다. 다만 기고는 린의 기반이 귀납적 구성의 미적분학(CIC)이라는 점을 소개한 뒤 끝나며, 향후 일정이나 비용 전망은 제시하지 않았다.