컴퓨터 보조 증명

수치해석 소프트웨어 마지막 수정: 2026-09-14 04:48:41

1. 개요[편집]

컴퓨터 보조 증명 Computer-Assisted Proof
두 갈래	대화식 증명 보조기 · 자동 증명기(SAT/SMT/ATP)
신뢰 기반	작은 커널이 증명 대상을 재검사 — de Bruijn 기준
이론 배경	커리-하워드 대응 · 의존 타입 이론 · 고차 논리
대표 도구	Rocq(구 Coq) · Isabelle/HOL · Lean · HOL Light · Mizar
이정표	4색정리(2005) · 홀수 차수 정리(2012) · 케플러 추측(2014)
소프트웨어	CompCert 검증 컴파일러 · seL4 커널
수치해석 접점	구간 해석 기반 검증 계산 · 부동소수점 알고리즘 검증
비용 지표	de Bruijn 계수 — 형식 증명 길이 / 원문 길이, 대략 4배

수학자가 “자명하다”고 쓴 자리에서 기계는 언제나 멈춰 선다. 그 자리가 진짜로 자명했던 적은 생각보다 적다.

컴퓨터 보조 증명(computer-assisted proof)은 증명의 일부 또는 전부를 컴퓨터가 수행하거나 기계적으로 검증한 수학적 증명이다. 크게 두 가지 다른 일이 이 이름으로 불리는데, 구분하지 않으면 논쟁이 헛돈다.

대규모 계산을 증명의 한 단계로 쓰는 것. 유한하지만 사람이 손으로 못 끝낼 경우 분석을 컴퓨터가 소진한다. 4색정리와 구간 해석 기반 검증 계산이 여기다.
증명 자체를 형식 언어로 적고 기계가 한 줄씩 검사하는 것. 추론의 모든 단계가 정해진 규칙의 적용임을 소프트웨어가 확인한다. 이쪽이 오늘날 말하는 형식화(formalization)다.

앞의 것은 “계산 결과를 믿을 수 있는가”를 묻게 하고, 뒤의 것은 그 질문에 답하는 방법이다 — 계산까지 포함해 전부 형식 체계 안에 집어넣으면 된다. 케플러 추측이 1998년에는 전자였다가 2014년에 후자가 된 것이 이 분야의 성장을 압축해 보여 준다. 시뮬레이션 하는 사람 입장에서 이 주제가 남 일이 아닌 이유도 같다. “수렴했으니 맞겠지”와 “이 구간 안에 해가 존재함이 증명됐다”는 전혀 다른 진술이고, 후자를 원할 때 이 도구들이 유일한 선택지다.

2. 두 갈래 — 대화식과 자동[편집]

대화식 증명 보조기(interactive theorem prover, proof assistant)는 사람이 증명 전략을 지시하고 기계가 그 결과가 규칙에 맞는지 확인하는 도구다. 사람이 큰 그림을 잡고 기계가 회계를 맡는 분업이라 보면 된다.

Rocq(2025년 3월 9.0 릴리스에서 Coq 에서 개명했다) — 귀납적 구성 계산(CIC) 기반의 의존 타입 이론. 증명이 곧 항(term)이고, 그 항을 커널이 타입 검사한다. SSReflect/Mathematical Components 라이브러리가 대수 쪽 대형 형식화의 기반이다.
Isabelle/HOL — 고차 논리(단순 타입 이론) 기반. LCF 전통의 설계로, 추상 타입 thm 의 값은 추론 규칙을 통해서만 만들어질 수 있다. 형식화 결과를 모아 두는 Archive of Formal Proofs 가 사실상의 공용 저장소다.
Lean — 2013년 레오나르도 데 모라가 시작했고 Lean 4에서 자기 자신을 구현하는 언어가 됐다. 커뮤니티 수학 라이브러리 mathlib 이 이 도구의 진짜 자산이다.
HOL Light — OCaml로 쓰인 극단적으로 작은 커널이 특징. 커널이 작을수록 신뢰 논증이 쉽다는 철학의 극단이고, 그래서 부동소수점 검증과 케플러 추측에 쓰였다.
Mizar — 1973년부터 이어진 가장 오래된 계보. 증명문이 수학 논문의 산문에 가장 가깝게 생겼다.

자동 증명기는 반대로 사람의 지시 없이 탐색한다. 명제 논리의 SAT 풀이기, 산술·배열·비트벡터 같은 이론이 붙은 SMT 풀이기(Z3, cvc5), 1차 논리의 초융합(superposition) 기반 ATP(Vampire, E)가 대표다. 강력하지만 표현력에 천장이 있어서, 진짜 수학 정리를 통째로 맡길 수는 없다.

실전에서는 둘을 붙여 쓴다. Isabelle의 Sledgehammer 는 현재 목표를 외부 ATP·SMT 여러 개에 동시에 던지고, 누군가 성공하면 그 증명을 Isabelle 커널이 받아들이는 형태로 재구성해서 들여온다. 외부 도구는 힌트를 찾는 데만 쓰고 신뢰는 주지 않는 구조다. 이 “탐색은 밖에서, 검증은 안에서” 패턴이 현대 증명 보조기 설계의 표준이 됐다.

3. 무엇을 믿는가 — 커널과 de Bruijn 기준[편집]

증명을 컴퓨터가 검사했다는 말은, 결국 그 검사 프로그램을 믿는다는 말이다. 그러면 왜 그것을 믿나. 답이 de Bruijn 기준이다.

증명기는 사람이 통독할 수 있을 만큼 작은 커널이 검사할 수 있는, 독립적인 증명 대상(proof object)을 생산해야 한다.

이 기준을 만족하면 신뢰 기반(trusted computing base)이 도구 전체가 아니라 커널 한 조각으로 줄어든다. 증명 탐색을 맡은 수십만 줄짜리 자동화 코드는 아무리 버그가 많아도 틀린 증명을 만들어 낼 수는 있어도 커널을 통과시킬 수는 없다. 자동화가 마음껏 공격적일 수 있는 이유이고, 형식화 커뮤니티가 커널 크기에 병적으로 집착하는 이유다. 1967년 니콜라스 더 브라윈의 Automath 에서 시작해 밀너의 LCF(1972)가 타입 시스템으로 이 보장을 강제하는 방법을 확립했다.¹

증명 대상이 실제로 무엇이냐는 커리-하워드 대응이 말해 준다. 명제는 타입이고, 증명은 그 타입을 가진 프로그램이다. $A \Rightarrow B$ 의 증명은 $A$ 의 증명을 받아 $B$ 의 증명을 돌려주는 함수고, 증명 검사는 타입 검사다. Rocq와 Lean은 이 대응을 곧이곧대로 구현해서 증명이 진짜로 실행 가능한 항이며, 거기서 프로그램을 추출할 수도 있다. Isabelle/HOL은 LCF 방식이라 증명 항을 반드시 남기지는 않지만 신뢰 논증의 구조는 같다.

남는 위험은 커널 바깥에 있다. 정리 진술이 의도한 수학인지(형식화 오류), 어떤 공리를 썼는지(배중률·선택공리·비구성적 원리), 그리고 컴파일러와 하드웨어. 형식화된 정리를 인용할 때 “그래서 그 theorem 문장이 진짜 우리가 아는 그 정리를 말하고 있냐”를 사람이 읽어 확인하는 절차는 끝내 남는다.

4. 이정표가 된 증명들[편집]

4색정리. 아펠과 하켄(1976)이 “피할 수 없는 집합”의 배치들을 컴퓨터로 소진해 증명했고, 당시 수학계는 읽을 수 없는 증명을 받아들여야 하는지를 놓고 갈라졌다. 로버트슨·샌더스·시모어·토머스(1997)가 경우 수를 633개로 줄여 검증을 쉽게 만들었고, 곤티에가 2005년 Coq 으로 그래프 이론 부분과 계산 부분을 통째로 형식화하면서 30년 묵은 논쟁을 닫았다. 여기서의 교훈이 결정적이다 — 컴퓨터 계산에 대한 불신은 더 나은 컴퓨터 검증으로 해소됐다.
홀수 차수 정리(파이트-톰프슨). 홀수 위수의 유한군은 가해군이라는 정리로, 원논문이 한 호를 통째로 채운 255쪽짜리다. 곤티에가 이끈 팀이 2012년 Coq/SSReflect 로 형식화를 완료했고, 분량이 15만 줄 규모다. 계산이 아니라 깊은 구조적 논증을 형식화한 사례라는 점에서 4색정리와 결이 다르다.
케플러 추측. 구를 가장 빽빽하게 쌓는 방법이 오렌지 가게 방식이라는 명제. 헤일스(1998)가 구간 해석과 선형계획 하계를 조합한 대규모 계산으로 증명했는데, 심사위원들이 몇 년 검토 끝에 “99% 확신하지만 완전히 확인하지는 못했다”는 전례 없는 코멘트를 남겼다. 헤일스는 이에 Flyspeck 프로젝트로 응수해 2014년 8월 HOL Light 와 Isabelle 로 전면 형식화를 끝냈다.² 심사가 불가능해지자 심사를 기계에 넘긴 사건이다.
조합론적 거대 증명. 불 피타고라스 삼조 문제(2016)나 슈어 수 5(2017)처럼 대규모 병렬 SAT 으로 해결된 것들은 SAT 풀이기 문서에서 다룬다. 증명 파일이 테라바이트 단위라 “검사할 수는 있지만 이해할 수는 없는 증명”이라는 논쟁을 다시 불렀다.

5. 소프트웨어를 증명하기[편집]

같은 도구가 수학 대신 프로그램을 겨누면 형식 검증이 된다.

CompCert — 르루아가 이끈 Coq 검증 C 컴파일러. “컴파일된 코드는 원본 C 프로그램의 관측 가능한 동작을 보존한다”는 정리가 증명돼 있다. 이게 얼마나 센 주장인지는 외부 검증으로 드러났는데, 양 외(2011)가 무작위 C 프로그램 생성기 Csmith 로 주요 컴파일러를 전부 두들겨 수백 개의 버그를 찾았을 때 CompCert의 검증된 부분에서는 잘못된 코드를 생성하는 버그가 나오지 않았다. 수치 코드 입장에서는 “최적화가 내 계산을 바꿔치지 않는다”는 보장이라 의미가 남다르다.
seL4 — 마이크로커널의 C 구현이 추상 명세를 만족함을 Isabelle/HOL 로 증명(2009). 만 줄 남짓한 C 코드에 증명은 그보다 한 자릿수 크다.

6. 수치해석과의 접점[편집]

이 문서가 심위키에 있는 진짜 이유가 이 절이다. 부동소수점으로 굴러가는 계산에서 증명이라는 단어를 쓸 수 있게 만드는 경로가 둘 있다.

첫째, 구간 산술로 근사를 봉쇄한다. 계산 결과를 하나의 값이 아니라 참값을 반드시 품는 구간으로 얻으면, 유한한 계산이 무한한 대상에 대한 엄밀한 진술을 낳는다. 부등식 $f(x) > 0$ 을 상자 위에서 검증하거나, 크라브칙 연산자로 “이 상자 안에 근이 정확히 하나 있다”를 확정하는 것이 전형이다. 기법의 세부는 구간 해석 문서에 있고, 이 경로로 나온 대표 결과는 이렇다.

란포드(1982) — 파이겐바움 재규격화 사상의 고정점 존재. 이 분야의 원형으로 꼽힌다. 자세한 것은 파이겐바움 상수.
터커(2002) — 로렌츠 방정식의 끌개가 실제로 쌍곡 이상끌개임을 증명해 스메일의 14번 문제를 해결했다. 반세기 동안 그림으로만 알려졌던 대상에 대한 첫 엄밀한 진술이었고, 카오스 이론에서 “수치가 이론을 앞서간다”는 상황을 수치가 스스로 끝낸 드문 사례다.
KAM 원환면과 불변 다양체의 존재 증명 — 근사해의 잔차를 구간으로 감싸 엄밀한 오차 한계를 얻는 방식. 매개화 방법 문서가 이 구조를 다룬다.

둘째, 부동소수점 알고리즘 자체를 형식 검증한다. 1994년 펜텀 FDIV 버그 이후 인텔은 해리슨의 HOL Light 를 써서 나눗셈·제곱근·초월함수 알고리즘의 정확도 한계를 기계 검증하는 쪽으로 갔다. Coq 쪽에는 IEEE 754 의미론을 통째로 형식화한 Flocq 라이브러리와 반올림 오차 한계를 자동으로 유도하는 Gappa 가 있고, CompCert 의 부동소수점 부분이 Flocq 위에 서 있다.

여기서 한 걸음 더 나간 것이 수치 해법 프로그램 전체의 검증이다. 볼도 외(2013)는 1차원 파동방정식을 푸는 C 프로그램에 대해 이산화 오차(수렴 차수)와 반올림 오차를 둘 다 형식적으로 한계 지은 증명을 Coq 으로 완성했다. 수치해석 교과서가 종이 위에서 하던 안정성·수렴성 논증과 부동소수점 연산의 오차 해석을 하나의 형식 증명 안에서 만나게 한 작업이라, 검증 및 확인의 언어로 말하면 verification 의 가장 강한 형태에 해당한다. 물론 대상이 1차원 파동방정식이라는 점이 이 접근의 현재 위치를 정직하게 말해 준다.

7. 라이브러리, 그리고 최근[편집]

형식화가 개인기에서 인프라 산업으로 바뀐 계기는 공용 라이브러리다. Lean 의 mathlib 은 정의와 정리 수십만 개를 한 저장소에 모아 매일 갱신되는 단일 체계로 굴린다. 군·환·위상·측도·범주까지 한 라이브러리 안에서 서로를 참조하므로, 새 정리를 형식화할 때 밑바닥부터 쌓을 필요가 없어졌다.

그 위력을 보여 준 사건이 Liquid Tensor Experiment 다. 2020년 12월 숄체가 자신의 응축 수학 결과 중 가장 확신이 덜 서는 정리를 지목해 형식화를 요청했고, 커뮤니티가 증명 구조를 잘게 쪼갠 청사진(blueprint)을 만들어 분업했다. 핵심 정리가 2021년에, 전체가 2022년 7월에 완료됐다. 여기서 중요한 것은 결과가 “맞았다”는 것보다, 형식화 과정이 증명의 진짜 골격이 어디인지를 드러냈다는 점 — 저자 본인이 자기 증명을 더 잘 이해하게 됐다고 밝힌 대목이다.

최근에는 탐색을 기계에 맡기는 쪽이 다시 뜨겁다. 대형 언어 모형으로 전술 후보나 증명 스케치를 생성하고, 그 결과를 Lean/Isabelle 커널에 던져 통과하는 것만 채택하는 구조다. de Bruijn 기준 덕분에 생성기가 아무리 헛소리를 해도 틀린 정리가 통과할 수는 없다는 점이, 이 조합이 유독 잘 맞아떨어지는 이유다. 검증이 값싸고 확실한 영역이라야 생성-검사 루프가 성립한다.

8. 한계와 반론[편집]

진술의 충실성. 커널이 통과시킨 것은 “그 형식 문장”이지 “그 수학”이 아니다. 정의를 잘못 적으면 참인 정리를 잘못된 대상에 대해 증명하게 된다. 형식화 논문에서 최종 정리 진술을 본문에 그대로 박아 놓는 관행이 그래서 생겼다.
공리와 커널 버그. Rocq 계열 도구에서도 커널 건전성 버그가 발견되고 수정돼 왔다. 실제로 악용된 사례는 없지만 “0% 위험”이 아니다. 여러 독립 검사기로 같은 증명 대상을 재검사하는 것이 현실적 대응이다.
비용. 비데이크가 제안한 de Bruijn 계수(형식 증명의 길이 / 원문의 길이)는 경험적으로 4 안팎이다. 즉 논문 한 편을 형식화하면 분량이 네 배가 되고, 그건 줄 수 이야기지 사람 시간 이야기가 아니다. 라이브러리가 좋아질수록 내려가지만 아직은 대형 프로젝트가 사람-년 단위를 먹는다.
읽을 수 없는 증명 문제는 안 없어졌다. 4색정리를 Coq 으로 형식화해도 사람이 왜 참인지 이해하게 되지는 않는다. 형식화가 답한 것은 “믿을 수 있는가”이지 “이해할 수 있는가”가 아니다. 이 둘은 다른 질문이고, 수학이 후자를 포기한 적은 없다.³

9. 관련 문서[편집]

LCF 의 설계가 남긴 부산물이 하나 더 있다. 밀너가 이 증명기를 조종할 메타언어로 만든 것이 ML 이고, 오늘날 OCaml·Haskell·Rust 로 이어지는 타입 시스템 계보의 출발점이 됐다. 증명 검사기를 안전하게 만들려다 프로그래밍 언어 하나가 튀어나온 셈인데, 이 바닥에서 부수적 성과가 본체를 압도한 대표적 사례다. ↩
이름은 “Formal Proof of Kepler”의 자음 F·P·K 를 품은 영어 단어에서 따왔다. flyspeck 은 파리똥만 한 얼룩, 또는 그런 것까지 샅샅이 뒤진다는 뜻의 동사다. 몇 년짜리 검증 프로젝트에 붙이기에 이보다 정확한 이름은 찾기 어렵다. ↩
4색정리 논쟁 당시의 반론이 “이건 증명이 아니라 실험 보고서다”였다. 50년이 지나 검증 문제는 깔끔하게 해결됐지만 이해 문제는 그대로고, SAT 으로 나온 조합론 증명들처럼 파일 크기가 테라바이트 단위로 가면 격차가 더 벌어진다. 기계가 통과시킨 증명 앞에서 “그래서 왜죠?”라고 물으면 아직 아무도 대답을 못 한다. 그리고 수학자가 원래 원하던 것은 늘 그 대답이었다. ↩