1976년 4색 정리, 컴퓨터가 증명한 첫 사례와 수학자들의 엇갈린 반응

AI가 짠 코드도 이제 사람이 한 줄씩 다 안 읽는 게 과정이 된 것 같음. 근데 나쁜 변경을 올린 사람 책임은 자동화해도 사람한테 남더라.

4색 정리는 참인 건 알았는데 왜 참인지는 몰랐던 게 문제임. 좋은 증명은 그 문제가 다른 문제랑 어떻게 엮이는지 알려주는데, 컴퓨터 증명은 true/false만 줌.

컴퓨터 증명 때문에 통찰 있는 증명을 찾는 연구가 오히려 줄었다는 얘기 있음. '증명은 됐는데 통찰은 없음' 상태를 열린 문제로 봐야 한다는 수학자도 있는 듯함. 나는 수학자 아님.

AI가 나중엔 우아한 설명도 찾아줄 거라 봄. 시간 문제 아닐까.

근데 무한한 그래프를 유한한 경우로 줄이는 과정 자체에 이미 통찰이 많이 들어감. 그걸 과소평가하면 안 됨.

tree-width 같은 개념도 원래 이 증명을 단순화하려고 나온 거임.

1980년대 초에 항공우주 회사에서 프로그램 검증기 만들 때 컴퓨터가 만든 증명 때문에 욕먹은 적 있음. Boyer-Moore 이론에서 배열 공리를 증명하려다 특수 케이스가 엄청 쏟아졌음.

ACL2 요즘 재밌게 보고 있는데, SBCL 위에서 돌아간다고 하더라.

이 증명이 케이스 쪼개기 없이 쉽고 이해 가능한 형태로 다시 나올 기회가 생긴 거임.