- Published on
2026년, 정리 증명기(proof assistant)는 더 이상 학계의 비밀 무기가 아니다. Lean 4는 Leonardo de Moura가 AWS로 옮긴 뒤 폭발적으로 성장했고, mathlib는 100만 개 정리를 넘기며 Terence Tao를 비롯한 일급 수학자들의 일상 도구가 되었다. Coq는 2024년 3월 Rocq로 리브랜드를 마쳤고, Agda·Idris 2·Isabelle/HOL은 각자의 자리를 지킨다. Microsoft의 F*는 HACL* 암호 라이브러리를 검증해 Firefox와 Linux 커널에 실제로 들어갔고, Liquid Haskell은 refinement type으로 일반 코드를 검증한다. 그 위로 AI가 올라탔다 — DeepMind AlphaProof는 IMO 2024에서 은메달을, Anthropic은 AIMO ($5M 상금)와 mathlib search에 합류했다. Terence Tao는 Lean과 GitHub Copilot으로 자기 논문을 형식화하고 있다. Z3·CVC5 SMT 솔버가 그 밑단을 받치고, seL4·CompCert·IronFleet는 형식 검증이 실제 시스템에서 작동함을 증명한다. 한국의 KAIST·ETRI, 일본의 京都大学·東京大学·AIST가 그 흐름을 따라간다. 이 글은 2026년 정리 증명기 생태계 전체를 한 자리에 정리한다.