개념
컴퓨터가 맡은 계산도 증명의 일부인가? 유한한 경우를 빠짐없이 환원해 검사하거나, 증명 보조기가 모든 논리 단계를 확인한다. 핵심은 많이 계산하는 것이 아니라 환원의 완전성과 독립 검증이다.
한 호흡으로 이해하기
"문제를 유한한 경우들로 빠짐없이 환원하고, 컴퓨터가 각 경우를 검증해 증명을 완성한다." 단순히 많은 예를 계산하는 것과는 다르다. 1976년 4색 정리, 케플러 추측의 Flyspeck 형식 검증(2014), 부울 피타고라스 삼중 문제(2016)가 대표적이다. 핵심 쟁점은 환원의 완전성과 프로그램·인증서를 얼마나 독립적으로 검증할 수 있는가이다.
한눈에 보기
연도 | 정리 | 컴퓨터의 역할 | 크기 |
|---|---|---|---|
1976 | 4색 정리 | 유한한 불가피 구성들을 프로그램으로 검사 | 당시로서는 대규모 계산 |
1996 | Robbins 추측 (불 대수) | EQP 자동 증명기 (McCune) | 8일 자동 탐색 |
1998 | 케플러 추측 (공 쌓기) | 5,000개 부등식 + LP | Hales 1998 → Flyspeck 2014 |
2014 | Flyspeck (Hales 검증) | Coq + HOL Light로 완전 형식 검증 | 수년의 협업 |
2016 | 부울 피타고라스 삼중 | SAT 솔버 | 계산 중 생성 자료 약 200 테라바이트 |
2021+ | Lean·Mathlib 생태계 | 정리와 라이브러리를 공동 형식화 | PFR 정리 형식화 등 다수 협업 |
컴퓨터 보조 증명의 신뢰는 “컴퓨터인가 아닌가”보다 환원의 완전성, 코드·인증서, 독립 재검증, 형식 체계의 작은 신뢰 기반을 어떻게 공개하느냐에 달려 있다.
핵심 식
유한한 경우로 완전하게 환원한 뒤 모든 경우를 검증하면 증명이 된다
핵심 순간
4색 정리 — 대규모 컴퓨터 보조 증명
아펠과 하켄이 유한한 경우 환원과 프로그램 검사를 결합했다. 사람이 계산 전체를 직접 읽기 어렵다는 점이 논쟁을 낳았다.
케플러 추측과 Flyspeck
헤일스의 컴퓨터 보조 증명은 이후 Flyspeck 프로젝트를 통해 2014년 형식 검증되었다.
부울 피타고라스 삼중 문제
SAT 솔버가 거대한 인증서를 만들었다. 결과를 믿는 근거가 프로그램·인증서·독립 검사로 나뉘는 사례다.
증명 보조기의 확산
Lean·Coq·Isabelle 같은 시스템이 대규모 수학 라이브러리와 연구 정리를 기계 검증 가능한 형태로 축적한다.
오늘날의 응용
4색 정리(1976), 케플러 추측과 Flyspeck 형식 검증, 부울 피타고라스 삼중 문제(2016), 소프트웨어·하드웨어의 형식 검증. 유한한 영점 검사는 추측의 증명과 구별한다.
MathVoyage 너머로
불러오는 중…