어떤 오류가 사소한 실수인가
요약
- 어떤 정의나 증명에 있는 오류가 고치기 쉽더라도 알아차리기 어렵다면, 그 실수는 사소하지 않습니다.
- 어떤 오류는 증명 보조기의 도움을 받아야 찾아낼 수 있습니다.
- 미래에 제가 수학적 개념을 새로 정의할 때는 증명 보조기로 그 개념의 주요 성질을 꼭 증명할 것입니다.
본문
지난해에 린(Lean) 정리 증명기의 수학 라이브러리 매스리브(Mathlib)를 린 3에서 린 4로 포팅[이식] 하는 작업에 저도 조금 참여했는데, 어쩌다 보니 제가 린 표준 라이브러리 Std에 있는 문자열 보조 정리 파일의 공저자가 됐습니다.
마리오 카네이로(Mario Carneiro) 박사 후 연구원님이 이 파일에 많은 보조 정리를 추가하셨고, 그중 열한 가지에는 진술과 증명 없이 "TODO(나중에 할 일)"라는 주석만 달렸습니다. 이 정리들을 증명하고자 할 사람은 저와 카네이로 연구원님 말고는 없을 테고, 카네이로 연구원님은 늘 바쁘시니 결국 제가 지난해 12월부터 작업을 시작했습니다.
첫째 문자열 정리 String.splitOn_of_valid
는 문자열 연산 String.splitOn
의 명세를 밝히기 위한 보조 정리입니다. 이 함수는 주어진 문자열에서 특정 부분이 나올 때마다 그 문자열을 가릅니다. 그 특정 부분을 제외한, 갈라진 문자열 조각들의 목록이 원래의 문자열에 대한 함숫값입니다.
예를 들어, 문자열 "abcabc"
에서 "bc"
가 나올 때마다 그 문자열을 가른 결과는 "a"
, "a"
, ""
입니다. splitOn
함수는 이 조각들의 목록인 ["a", "a", ""]
을 산출합니다.
이 첫째 문자열 정리를 증명하는 데 170시간 정도가 걸릴 줄은 저도 전혀 예상하지 못했습니다. 지난해 12월에 증명을 작성하기 시작해서 올해 4월 16일에 완성했습니다. 아쉽게도, 170시간 가운데 67시간 정도는 제가 정리를 잘못 진술해서 헛고생했습니다. 올해 1월 3일에 마리오 카네이로 연구원님의 도움을 받아 제대로 된 진술을 작성할 수 있었고, 그 뒤로 93시간 정도 증명을 시도한 결과 splitOn
함수의 정의에 버그가 있다는 사실을 깨달았습니다. 카네이로 연구원님이 버그를 고치신 뒤에 제가 증명을 완성하는 데는 10시간 남짓 걸렸습니다.
저는 이 오류가 너무 섬뜩했어요. splitOn
함수는 대개 똑바로 작동했기 때문입니다. 그래서 정리 splitOn_of_valid
를 증명하려고 시도할 때마다 증명의 대부분은 작성할 수 있었지만, 마지막 경우의 부분 증명은 자꾸 실패했습니다. 나중에야 특정 부분 증명의 목표가 거짓인 것 같다는 생각이 들었습니다. 제가 진술한 정리는 참이라는 확신이 있었기 때문에 splitOn
함수의 정의가 잘못됐을 수도 있다는 의심을 품었죠.
digama0 said:
The code change here is very small, replacing a
i
withi - j
, but it makes termination more complex so that's where the rest of the line count goes.
이 버그를 고치는 일은 그리 어렵지 않았습니다. 해당 정의에서 i
를 i - j
로 바꾸기만 하면 됐어요. 그렇다고 해서 이 오류가 사소한 실수였다고 생각하지는 않습니다. 이 정의에 따르면 splitOn
함수가 대개 올바로 작동하지만, 특수한 경우에는 잘못된 결과를 산출하니까요.
린 같은 증명 보조기를 이용하지 않았다면, 이렇게 미묘한 오류를 저는 절대로 못 찾아냈을 것입니다. 린으로 어떤 함수를 정의하고 나서 그 함수의 성질을 형식적으로 증명할 수 있었기 때문에 그 정의가 정확한지를 제가 판단할 수 있었습니다. 덧붙여 말하면, 마우리치오 콜라레스(Maurício Collares) 님이 splitOn
함수의 이런 작동 방식을 지난해 6월에 이미 알고 있었지만, 그분은 이 작동 방식을 버그라고 생각하지 않았어요.
미래에 제가 수학 이론을 본격적으로 형식화할 때는 이번처럼 정의상의 오류를 또 발견할 가능성이 작을 듯합니다. 수학자들은 보통 어떤 개념을 정의하고 나서 그 개념의 주요 성질을 증명하기 때문이죠. 하지만 저는 새로운 수학적 개념을 정의할 때마다 꼭 증명 보조기를 이용해 그 개념에 대한 여러 보조 정리를 증명할 것입니다. 미묘하지만 사소하지 않은 실수를 제가 저질렀을 때, 제 주변의 수학 전공자보다 증명 보조기가 제 실수를 더 뚜렷이 드러낼 테니까요.