형식 증명이란 — AI의 수학을 '믿을 수 있게' 만드는 장치
Formal proofs explained: the machinery that makes AI mathematics verifiable
증명을 컴퓨터가 기계적으로 검사할 수 있는 코드로 쓰는 것으로, AI 결과물의 '그럴듯한 오답'을 차단한다
3줄 요약
- 형식 증명은 논리 전개를 Lean 같은 언어의 코드로 써서 컴퓨터가 전 단계를 검사하게 한다
- 사람 심사는 몇 달 걸리고 실수가 있지만, 형식 검증은 통과하면 논리적 빈틈이 없다
- AI가 만든 증명의 신뢰 문제를 푸는 열쇠 — 오픈AI 수학 발표의 기둥이 이것이다
핵심 질문
- 형식 증명이 일반 증명과 뭐가 달라
- 일반 증명은 사람이 읽는 글이고, 형식 증명은 컴퓨터가 검사하는 코드다. 증명의 모든 논리 단계를 Lean, Coq 같은 증명 보조 언어의 문법으로 쓰면, 검증기가 공리에서 결론까지 빈틈없이 이어지는지를 기계적으로 확인한다. '대충 넘어가는' 단계가 원리적으로 존재할 수 없다.
- 왜 AI 시대에 갑자기 중요해졌어
- AI의 고질병이 '자신 있는 헛소리'라서다. AI가 내놓은 증명이 그럴듯해 보여도 어딘가 논리 구멍이 있을 수 있는데, 사람이 일일이 찾기엔 양이 많고 어렵다. 형식 증명은 이 검증을 기계에 맡긴다 — 검증기를 통과한 증명은 AI가 썼든 사람이 썼든 논리적으로 참이다. 오픈AI가 수학 성과를 Lean 코드로 공개한 이유다.
- 그럼 모든 수학이 형식 증명으로 가는 거야
- 방향은 그쪽인데 비용이 문제였다. 사람 수학자가 형식화하면 종이 증명의 몇 배 노력이 들어 극히 일부만 형식화돼 왔다. 반전은 그 형식화 작업 자체를 AI가 잘한다는 것 — AI가 증명하고 AI가 형식화하며 기계가 검증하는 순환이 열리면, 수학의 검증 속도 자체가 바뀐다.
오늘 오픈AI 수학 기사에서 "형식 증명이 이 발표의 기둥"이라고 썼다. 그 기둥을 뜯어보는 것이 이 문서다. 형식 증명(formal proof)은 AI 시대 이전엔 수학의 골방 취급을 받던 분야였는데, AI가 수학을 하기 시작하면서 갑자기 무대 중앙에 섰다 — '기계가 만든 답을 어떻게 믿나'라는 시대의 질문에 대한, 지금까지 나온 가장 단단한 답이기 때문이다.
1. 개념 — 읽는 증명에서 검사받는 증명으로
수학 증명은 전통적으로 사람이 읽는 글이다. 동료 수학자들이 논문을 읽고 논리를 따라가며 심사하는데, 이 과정은 몇 달씩 걸리고 실수도 있다 — 유명 정리의 증명에서 수년 뒤 구멍이 발견된 사례가 실제로 있다.
형식 증명은 접근을 바꾼다. 증명의 모든 논리 단계를 Lean, Coq, Isabelle 같은 증명 보조기(proof assistant) 언어의 코드로 쓴다. 그러면 검증기가 공리에서 출발해 결론까지, 모든 추론 단계가 허용된 규칙만으로 이어지는지를 기계적으로 검사한다. 사람 심사의 "이 부분은 자명하니 넘어간다"가 원리적으로 불가능하다 — 자명해 보이는 단계도 코드로 채워야 컴파일이 통과된다.
2. 비교 한눈에 — 그리고 AI가 바꾼 계산
| 항목 | 전통 증명 (사람 심사) | 형식 증명 (기계 검증) |
|---|---|---|
| 형태 | 자연어 논문 | 증명 보조기 코드 |
| 검증 주체 | 동료 수학자 | 검증 프로그램 |
| 소요 시간 | 수개월~수년 | 컴파일 즉시 |
| 오류 가능성 | 심사자도 놓칠 수 있음 | 통과 시 논리 빈틈 없음 |
| 작성 비용 | 낮음 | 매우 높음 — 이게 보급의 병목이었다 |
| AI 이후 | — | 형식화 자체를 AI가 수행 시작 |
표의 마지막 두 줄이 지금 벌어지는 변화다. 형식 증명의 유일한 약점은 작성 비용이었다 — 사람이 종이 증명을 형식화하려면 몇 배의 노력이 들어, 수학 전체에서 형식화된 부분은 극히 일부였다. 그런데 이 지루하고 엄밀한 번역 작업을 AI가 잘한다. AI가 증명을 만들고, AI가 형식화하고, 기계가 검증하는 순환이 열리면 '증명 검증'이라는 수학의 병목 자체가 사라진다. 오픈AI가 미해결 문제의 성과를 Lean 코드로 깃허브에 올린 것은 이 순환의 공개 시연인 셈이다.
3. 남은 것 — 이 문서의 사용법
앞으로 "AI가 수학 문제를 풀었다"는 뉴스를 볼 때 확인할 것은 하나다 — 형식 증명이 공개됐는가. 공개됐다면 누구든 검증기를 돌려 참·거짓을 확인할 수 있으니 발표 주체를 믿을 필요 자체가 없고, 자연어 증명뿐이라면 학계 심사가 끝날 때까지 판단을 미루면 된다. 이 잣대 하나가 과장과 실적을 가른다. 이번 사례는 「AI가 수학 미해결 문제 10개를 건드렸다」에서, AI 검증의 다른 축(안전성)은 「백악관 AI 검증 프레임워크」에서 이어진다.