컴퓨터가 수학자를 이긴 첫 순간: 4색 정리 증명
The Four Colour Theorem: The first time machines mogged mathematicians
1976년 7월, 100년 넘게 수학자를 괴롭혀온 4색 정리가 마침내 증명됐다. Kenneth Appel과 Wolfgang Haken은 컴퓨터로 1,200시간, 100억 번의 결정을 내려 증명의 상당 부분을 처리했다. 일부 수학자는 이를 오라클에 의존한 증명이라며 거부했고, 나이 든 수학자일수록 컴퓨터 증명을 불신했다. 이 사건은 인간과 기계가 함께하는 수학의 서막을 열었다.
“신은 그렇게 끔찍한 방법으로 정리가 증명되도록 내버려두지 않으실 거야!” - Herbert Wilf, University of Pennsylvania
HN 토론
25- fhdkweig
증명의 문제점은 FCT가 참이라는 건 알았지만 왜 그런지는 전혀 몰랐다는 거였다. 좋은/우아한 증명은 그 문제가 다른 문제들과 어떻게 연관되는지에 대해 새로운 것을 가르쳐준다. 단지 추측에 대한 참/거짓 답을 얻는 게 전부가 아니다.
- layer8
우리가 이미 타임머신을 발명했는지 몰랐네. ;)
- jjtheblunt
제목을 보니 계산에 사용된 훨씬 오래된 기계가 생각났다