AI가 증명을 다 써내도 설명 못 하면 미완성이다

지도에서 이웃한 나라를 다른 색으로 칠하는 데 네 가지 색이면 충분하다. 수학자가 경우를 잘게 나누고 컴퓨터가 그것을 하나씩 검사해 증명해낸 명제다. 결론은 맞았지만 검사를 손으로 따라간 사람은 없었고 이것을 증명이라 불러도 되느냐는 물음이 남았다.

그 물음이 이번에는 훨씬 큰 규모로 돌아왔다. 수학자들은 증명을 기계가 읽을 수 있는 언어인 Lean으로 옮겨 적기 시작했다. 사람이 눈으로 훑는 대신 기계가 한 줄씩 확인한다. 초안을 쓰는 쪽에는 AI가 들어와 자리를 잡았다. 묻힌 정리를 문헌에서 찾아내는 속도는 이미 사람이 따라가기 어렵다. 증명의 초안을 통째로 내놓는 일도 드물지 않다.

그러자 무엇이 어려운 일인지가 뒤바뀌었다. 증명이 맞는지 확인하는 비용은 기계 검사로 크게 내려갔다. 반면 그 증명이 무슨 일을 한 것인지 알아내는 비용은 그대로다. 어떤 문제를 붙잡을지도 계산에 드는 비용이 먼저 정하는 형편이 됐다.

필즈상을 받은 수학자 테런스 타오가 이달 17일 arXiv에 올린 "인공지능 시대의 수학"은 이 문제를 정면으로 다룬다. 이 글은 AI가 쓴 증명이 "사소한 대목에 길게 머물고 새로운 대목은 짧게 지나가거나 오히려 가린다"고 적었다.

여기서 판이 둘로 갈린다는 전망이 나온다. 기계가 결과를 계속 쌓아 올리고 사람은 그중 일부만 취미처럼 이해하는 쪽이다. 다만 이해를 빼면 남는 것이 결과 하나뿐이라는 반론도 만만치 않다. 수학이 해온 일은 답을 얻는 데서 끝나지 않았다. 얻은 방법을 다음 문제로 옮기는 일이 늘 뒤따랐다.

타오가 내놓은 기준은 단순하다. 저자가 자기 결과를 정확하게 출처까지 밝혀 가며 전문가 앞에서 분명하게 설명하지 못한다면 그 결과는 발표하지 않는 편이 낫다는 것이다. 기계가 형식적으로 검증했더라도 아무도 설명하지 못하는 증명은 미완성이라고 적었다. 지도 한 장을 칠하는 문제에 걸려 있던 물음이 이제 수학이 무엇을 발표할 수 있고 무엇을 미완성으로 남겨 둘지까지 정하는 자리로 올라왔다.