그래프 이론에서 유명했던 문제 중 ‘4색 문제’가 있다. ‘인접한 지역을 서로 다른 색깔로 칠하는 규칙으로 모든 지도를 칠하는 데 네 가지 색이면 충분하다’ 언뜻 보면 무척 간단해 보이는 이 명제가 수많은 수학자를 괴롭혔다.

컴퓨터를 이용해 증명

4색 정리는 비교적 간단해 보이는 증명이라 수많은 아마추어 수학자들이 증명했다고 주장했지만 제대로 된 증명은 없었다. 1930년, 쿠라토프스키는 모든 평면 그래프를 5가지 색으로 칠할 수 있다는 것을 증명했다.
독일의 수학자 헤슈는 난항을 겪던 4색 문제 증명을 컴퓨터로 하자는 아이디어를 냈고, 증명의 기본 뼈대를 세웠다. 이를 토대로 미국 수학자 아펠과 하켄은 평면 그래프를 유형별로 나누고 각각의 경우를 계산해 줄 알고리즘을 만들었다. 그 후, 만들어진 알고리즘으로 컴퓨터에 연산을 맡겼다. 오랜 시간 동안 컴퓨터는 연산을 수행했고 1976년 8월, 컴퓨터가 연산을 멈추는 순간 증명도 끝났다.

컴퓨터를 이용한 증명에 대한 반감

아펠과 하켄의 컴퓨터를 이용한 증명은 반발도 많았다. 컴퓨터를 이용한 최초의 증명이라는 점에서 몇몇 수학자들의 회의적인 시선도 있었다. 컴퓨터를 이용해 수많은 가능성을 모두 반복 검토하는 작업은 우아하고 아름다운 수학과 동떨어져 있다는 견해였다. 한편으로는 증명에 오류가 있을 것이라 생각하는 사람도 있었다.
하지만 알고리즘에는 문제가 없었고, 4색 정리는 분명히 증명되었다. 이후로 아펠과 하켄의 증명을 조금 더 간결하게 하는(가짓수를 줄이는) 데는 성공했지만, 여전히 컴퓨터의 힘을 빌리지 않은 증명은 나오지 않고 있다.

아직 연구할 부분 많아

4색 정리는 증명의 난이도에 비해 실용적인 응용 가능성은 높지 않다. 하지만 이 증명을 위해 수많은 수학자가 고뇌하며 만들어낸 그래프 이론 등의 성과는 수학적으로 중요한 의미가 있다. 또한, 4색 정리는 증명되었다는 것으로 끝난 것이 아니다. 아직 더 확장해서 연구하고 고민할 문제들이 많다.