개념
평면 지도를 인접한 두 영역이 다른 색이 되게 칠할 때 네 색이면 충분하다. 1852년의 질문은 1976년 방대한 경우를 컴퓨터로 검사한 첫 대표적 증명으로 해결돼 검증 가능성 논쟁을 낳았다.
한 호흡으로 이해하기
모든 평면 지도는 단 4가지 색만으로 인접한 두 영역이 다른 색을 갖게 칠할 수 있다. 1852년 한 학생이 형에게 던진 질문은 1976년 아펠과 하켄이 논증을 유한한 경우들로 환원하고 컴퓨터로 검증하면서 해결됐다. 컴퓨터에 의존해 증명된 첫 주요 정리로 널리 꼽히며, "사람이 끝까지 직접 확인할 수 없어도 증명인가?"라는 논쟁을 크게 만들었다.
한눈에 보기
연도 | 인물 | 진전 |
|---|---|---|
1852 | Francis Guthrie | 동생의 질문: 영국 지도를 칠하다 발견 |
1879 | Kempe | 거짓 증명 제출 — 11년간 정설 |
1890 | Heawood | Kempe 증명의 결함 발견; 5색 정리 증명 |
1976 | Appel + Haken | 컴퓨터로 1,936 케이스 검증 — 1,200시간 CPU |
1996 | Robertson 등 | 633 케이스로 증명 단순화 |
2005 | Gonthier | Coq에서 형식 검증 — 완전 기계 검증 |
컴퓨터 보조 증명의 이정표 — 사람이 모든 계산을 손으로 되짚기 어려운 첫 주요 정리였다. 이후 더 단순한 증명과 형식 검증이 이어졌다.
핵심 식
평면 지도는 4색이면 충분
핵심 순간
학생의 질문
프랜시스 거스리가 영국의 주(county) 지도를 색칠하며 네 색이면 충분한지 물었고, 동생을 통해 드모르간에게 질문이 전해졌다.
켐페 — 잘못된 증명
아서 켐페가 증명을 발표. 11년 동안 옳다고 믿어짐. 1890년 결함 발견.
아펠·하켄 — 컴퓨터로 경우를 검사
논증을 유한한 구성 목록으로 환원하고 프로그램으로 검사했다. 컴퓨터에 본질적으로 의존한 첫 주요 정리로 널리 꼽히며, 검증 가능성을 둘러싼 논쟁을 일으켰다.
오늘날의 응용
주파수 할당, 시간표 작성, 컴파일러의 레지스터 할당, GIS 지도 색칠, 충돌 회피.
MathVoyage 너머로
불러오는 중…