Lean

증명 보조기(proof assistant)이자 함수형 프로그래밍 언어입니다. 마이크로소프트 리서치의 Leonardo de Moura가 2013년에 시작했습니다. 수학적 논증의 각 단계를 기계가 검사해서, 증명이 소수의 공리에서 실제로 따라 나오는지 알고리즘으로 확인합니다.

핵심 자산은 Mathlib입니다. 커뮤니티가 형식화해 온 수학 표준 라이브러리이고, 새 증명은 여기 정의된 정리 진술과 대조할 수 있습니다. 진술 자체가 어긋나면 증명이 아무리 통과해도 다른 정리를 증명한 것이라, 이 대조가 중요합니다.

AI 증명의 검증 수단

LLM이 생성한 증명은 사람이 읽어서 검증하기 어렵습니다. 분량이 크고 서술이 기계적이라 학계의 통상적인 심사 절차가 잘 작동하지 않습니다. 그래서 2026년 들어 AI 수학 결과 발표는 대체로 Lean 인증서를 함께 냅니다.

Anthropic의 페르마 마지막 정리 형식화는 Claude가 11일간 Lean 코드 1,300만 줄을 써서 중간 정리 29,500개를 증명한 결과이고, Lean이 이를 표준 공리 세 개에 대해 검사했습니다. OpenAI의 나비에-스토크스 발표도 165쪽 증명과 Lean 형식화를 함께 공개했습니다. 트리스탄 벅마스터와 Levent Alpöge 역시 Lean 검증을 마친 결과만 내놓았습니다.

Lean이 보장하는 것은 증명의 논리적 정합성입니다. 그 증명을 누가 먼저 떠올렸는지, 모델이 무엇을 보고 만들었는지는 검사하지 않습니다. 이 구분이 OpenAI가 나비에-스토크스를 풀었다는 발표와, 그 뒤에 붙은 크레딧 분쟁의 핵심입니다.