증명 보조기(Proof assistant)

'A이고 B이면, B이고 A이다'를 증명한다고 해 봅시다. 종이에서는 한 줄로 끝납니다. 증명 보조기 Lean에서는 아래처럼 한 걸음씩 적고, 걸음마다 컴퓨터가 지금 가진 가정과 남은 목표를 보여 줍니다. 목표가 모두 사라지면 증명이 끝납니다. 끝에 남는 것은 $\mathsf{fun}\ \langle a, b\rangle \Rightarrow \langle b, a\rangle$라는 프로그램, 곧 쌍의 두 성분을 맞바꾸는 함수입니다. 증명 보조기는 이 프로그램의 타입⁠(type)⁠이 $A\land B\to B\land A$인지 검사합니다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠에 따라 증명을 검사하는 일이 타입을 검사하는 일이 되는 것입니다.

증명할 명제는 입니다.

믿어야 할 것을 줄이기. 증명 보조기에서 사람이 적는 것은 대개 전술(tactic)입니다. 'intro h'나 'induction n'처럼 증명을 어떻게 만들지 지시하는 명령이고, 자동화된 전술은 긴 계산이나 뻔한 단계를 대신 채웁니다. 전술을 실행하는 프로그램은 크고 복잡해서 틀릴 수 있습니다. 그래서 전술은 결국 증명 항을 내놓고, 그 항을 작은 검사 핵심(커널)이 타입 규칙대로 다시 검사합니다. 이 구조 덕분에 믿어야 할 코드가 커널 하나로 줄어듭니다. 증명을 작은 독립⁠(independence)⁠ 프로그램이 확인할 수 있는 형태로 남겨야 한다는 이 원칙을 더 브라위언 기준⁠(de Bruijn criterion)⁠이라 부릅니다(Automath를 만든 더 브라위언의 이름을 딴 것입니다). 다른 길은 1970년대 밀너의 LCF가 연 방식입니다. '정리'를 하나의 추상 타입으로 두고 그 값을 만드는 함수⁠(function)⁠를 추론 규칙들로만 제한하면, 아무리 복잡한 전술을 써도 규칙을 우회해 정리를 만들 수 없습니다. 이 전술들을 안전하게 적으려고 만든 언어가 ML이고, ML을 위해 다듬어진 것이 힌들리–밀너 타입 추론⁠(type inference)⁠입니다.

증명 보조기는 바탕으로 삼는 논리에 따라 갈래가 나뉩니다. Automath(1967년 무렵), Coq(1989년 첫 공개, 2025년 Rocq로 이름을 바꿈), Agda, Lean(2013년 시작)은 의존 타입⁠(dependent type)⁠ 이론 위에 서 있습니다. HOL 계열(HOL Light, Isabelle/HOL)은 처치의 단순 타입 이론⁠(type theory)⁠에서 나온 고차 논리를, 폴란드의 Mizar(1973년 시작)는 집합론⁠(set theory)⁠을 씁니다. 어느 쪽이든 원리는 같습니다. 증명은 공리⁠(axiom)⁠에서 출발해 추론 규칙을 한 번씩 적용해 가는 유한한 기호열이고, 규칙을 지켰는지 확인하는 일은 기계적입니다.

검사할 수 있는 것과 없는 것. 증명을 검사하는 일은 기계적이지만 증명을 찾는 일은 다릅니다. 1차 논리⁠(first-order logic)⁠의 문장이 증명 가능한지 판정하는 일반적인 방법이 없다는 것이 1936년 처치와 튜링의 결과입니다(정지 문제⁠(halting problem)⁠와 같은 종류의 불가능성). 증명이 있다면 기호열을 짧은 것부터 차례로 검사해 언젠가 찾을 수는 있지만, 증명이 없을 때는 이 탐색이 끝나지 않고, 있을 때도 대개 너무 오래 걸립니다. 그래서 증명 보조기에 들어가는 증명의 뼈대는 대부분 사람이 적습니다. 답을 확인하기는 쉬운데 찾기는 어려워 보인다는 이 모양은 P 대 NP 문제⁠(P versus NP problem)⁠의 모양과도 닮았습니다. 또 검사를 통과한 증명이 보증하는 것은 '적어 넣은 형식 명제가 체계의 공리에서 따라 나온다'까지입니다. 형식 명제가 사람이 뜻한 명제와 다르게 적혔다면, 예컨대 정의를 잘못 옮겼다면 검사는 그것을 잡지 못합니다. 커널이나 하드웨어의 결함도 드물지만 실제로 발견되어 고쳐진 적이 있습니다. 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠도 그대로 적용됩니다. 증명 보조기의 논리처럼 산술을 담을 만큼 강한 체계는, 모순이 없다면 참이지만 체계 안에서 증명할 수 없는 문장을 가지며 자기의 무모순성⁠(consistency)⁠을 증명하지 못합니다.

이정표. 4색 정리⁠(four color theorem)⁠는 1976년 케네스 아펠과 볼프강 하켄이 컴퓨터로 수많은 배치를 확인해 증명했지만, 사람이 다 따라갈 수 없는 계산 때문에 오래 의심을 받았습니다. 2005년 조르주 공티에와 뱅자맹 베르네르가 증명 전체를 Coq로 형식화했고, 그 뒤로는 경우를 확인하는 여러 특수한 프로그램이 아니라 Coq의 커널만 믿으면 됩니다. 공티에가 이끈 팀은 2012년 9월, 원래 논문이 255쪽에 이르던 파이트–톰프슨 정리(원소⁠(element)⁠가 홀수 개인 유한군⁠(finite group)⁠은 가해군⁠(solvable group)⁠, 곧 아벨군 조각들로 차례로 쪼갤 수 있는 군이다)의 형식화를 6년 만에 마쳤습니다. 증명 스크립트만 15만 줄이 넘었습니다.

같은 크기의 공을 가장 빽빽하게 쌓는 방법은 과일 가게에서 오렌지를 쌓는 방식(공이 차지하는 부피의 비율 $\pi/\sqrt{18}\approx 0.7405$)이라는 케플러의 추측은, 1998년 토머스 헤일스가 방대한 컴퓨터 계산으로 증명했지만 심사위원들은 '99% 확신한다'고만 말할 수 있었습니다. 헤일스는 이 불확실성을 없애려고 Flyspeck 계획을 시작했고, 2014년 8월 HOL Light와 Isabelle로 형식 증명을 완성했습니다. 2020년 12월 피터 숄체는 더스틴 클라우젠과 함께 증명한 응축 수학⁠(condensed mathematics)⁠의 핵심 정리가 너무 섬세해 스스로도 확신하기 어렵다며 형식화를 제안했습니다(액체 텐서⁠(tensor)⁠ 실험). 요한 코멀린이 이끈 Lean 사용자들이 2021년 6월 핵심 부분을, 2022년 7월 전체를 검사했습니다.

기계가 찾은 증명. 형식 증명은 기계로 확인할 수 있다는 점 때문에 인공지능⁠(artificial intelligence)⁠ 연구와도 이어집니다. 언어 모델⁠(language model)⁠이 자연어로 쓴 증명은 그럴듯해도 틀릴 수 있지만, 커널을 통과한 형식 증명은 적어 넣은 명제에 관한 한 그런 걱정을 거의 없애 줍니다. 2024년 7월 구글 딥마인드는 강화 학습⁠(reinforcement learning)⁠으로 훈련한 AlphaProof가 그해 국제 수학 올림피아드 6문제 가운데 3문제의 Lean 증명을 찾았고, 기하⁠(geometry)⁠ 전용 체계 AlphaGeometry 2가 1문제를 더 풀어 42점 만점에 28점, 은메달 수준에 이르렀다고 발표했습니다. 다만 문제를 형식 명제로 옮긴 것은 사람이었습니다. 또 발표에 따르면 한 문제는 몇 분 만에 풀었지만 나머지에는 사흘까지 걸렸습니다(참가자에게는 이틀 동안 하루 4시간 30분이 주어집니다). 자연어 수학을 형식 명제로 옮기는 일(자동 형식화⁠, autoformalization⁠)은 아직 열린 과제입니다.

흔한 오해. '컴퓨터가 증명했다'와 '컴퓨터가 검사했다'는 다릅니다. 위의 이정표는 대부분 사람이 먼저 증명을 알고, 그것을 몇 년에 걸쳐 기계가 읽을 수 있게 옮긴 것입니다. 형식화의 가치는 새 정리를 찾는 데보다 오류를 잡고, 증명에 쓰인 가정을 빠짐없이 드러내고, 다시 쓸 수 있는 정의와 정리의 라이브러리(Lean의 mathlib 같은)를 쌓는 데 있습니다. 또 형식 증명도 '100% 확실'한 것은 아닙니다. 커널, 하드웨어, 그리고 형식 명제를 옮긴 사람의 판단은 여전히 믿어야 합니다. 다만 믿어야 할 것이 작고 분명해집니다.

이어지는 곳. 증명 검사가 타입 검사가 되는 원리는 커리–하워드 대응이고, Coq·Lean·Agda가 쓰는 논리는 의존 타입 이론입니다. 위 그림의 두 번째 증명은 의존 타입 페이지의 되부르는 증명과 같은 모양이라, 수학적 귀납법⁠(mathematical induction)⁠이 도구 안에서 어떻게 보이는지 견주어 볼 수 있습니다. 일가성을 계산하는 입방 타입 이론은 Cubical Agda로 구현되어 호모토피 타입 이론⁠(homotopy type theory)⁠을 직접 실험하게 해 줍니다. 1976년의 4색 정리가 불러일으킨 '컴퓨터 증명을 믿을 수 있는가'라는 물음에 약 30년 뒤 나온 답이 형식화였습니다. 증명을 찾는 일의 한계는 정지 문제와 불완전성 정리⁠(incompleteness theorem)⁠가 긋습니다. 형식 체계⁠(formal system)⁠로 수학 전체를 세우고 그 무모순성을 보이려던 힐베르트의 계획은 괴델의 정리 때문에 원래 모습대로는 이룰 수 없게 되었지만(수학 기초론 논쟁⁠, debate on the foundations of mathematics⁠), '증명은 기계가 확인할 수 있는 기호열'이라는 그의 생각은 증명 보조기로 살아 있습니다. 람다 계산⁠(lambda calculus)⁠의 항이 증명이 되고, 그 항을 검사하는 일이 타입 이론의 규칙을 따르는 일입니다. 반복문 옆에 불변식과 변량을 적는 다프니 같은 검증 도구는 호어 논리⁠(Hoare logic)⁠의 방식을 따르고, Lean과 Rocq가 귀납적으로 정의한 타입마다 자동으로 만드는 재귀자⁠(recursor)⁠는 시작 대수의 fold를 결과의 타입이 입력에 따라 달라지도록 넓힌 것입니다.