컴퓨터를 이용한 증명

컴퓨터를 이용한 증명은 수학적 증명 과정에 컴퓨터를 이용한 계산이 포함되어 있는 경우를 의미한다. 대표적인 경우로 4색정리가 있다.

증명 과정에서 컴퓨터를 이용하는 경우는 보통 사람이 직접 계산하기에는 힘든 것을 컴퓨터로 대신 처리하는 경우로, 예를 들어 4색 정리의 경우 무한개의 지도를 약 1500개의 경우로 분류한 다음 각각의 경우를 컴퓨터로 모두 계산해, 1200시간을 들여 검증했다.

이러한 증명의 가장 큰 문제점은 컴퓨터가 처리한 계산에 오류가 없는지 검증하는 것이 거의 불가능하다는 것이다. 검증을 위한 프로그램과 그 프로그램을 실행하는 CPU에 버그가 들어있을 수도 있기 때문에 잘못된 결론이 나올 수 있다는 것이다.

또한 이러한 방식의 증명은 수학적 발전에 도움이 거의 되지 않기 때문에 좋은 증명이 아니라는 비판이 있다. 필립 데이비스는 4색 정리를 컴퓨터로 증명했다는 것에 대해 '결국 [그 문제는] 좋은 문제가 아니었다'고 언급했다.