증명 보조기 Rocq가 명저 대수학 교과서의 오류를 잡아낸 방법

수학과 교재로 널리 쓰이는 더밋(Dummit)과 푸트(Foote)의 『Abstract Algebra』는 추상대수학 입문서 가운데 손꼽히는 권위서다. 그런데 최근 한 개발자가 리커스 센터(Recurse Center)에서 보낸 둘째 주에 이 책을 증명 보조기(proof assistant)인 Rocq로 형식화하려다, 책의 첫 번째 증명 연습문제에 실린 명제 자체가 참이 아니라는 사실과 마주쳤다. 손으로 풀었다면 그냥 넘어갔을 법한 구석진 사례가, 기계적 증명을 시도하는 과정에서 드러난 것이다.

문제의 명제는 간단하다. "함수는 단사(injective)일 필요충분조건이 좌역원(left inverse)을 가지는 것이다." 여기서 함수 f: A → B는 정의역과 공역 사이의 짝(pair)들의 집합으로 정의되며, 단사란 서로 다른 두 입력이 같은 출력으로 가지 않는 성질을 뜻한다. 예컨대 f(x) = x²는 f(1)과 f(-1)이 모두 1이 되므로 단사가 아니다. 좌역원은 f를 "되돌리는" 함수 g: B → A, 즉 A의 모든 원소 a에 대해 g(f(a)) = a를 만족하는 g가 존재한다는 의미다.

빈 집합이 만든 반례

명제가 무너지는 지점은 정의역이 비어 있을 때다. A를 공집합, B를 원소 하나짜리 집합 {1}이라 하고, f를 빈 함수(짝이 하나도 없는 집합)라고 두자. 이 f는 함수의 세 가지 정의 조건을 모두 만족하므로 엄연한 함수다. 게다가 "서로 다른 두 입력이 같은 출력으로 가지 않는다"는 조건은, 애초에 입력이 하나도 없으므로 공허하게(vacuously) 참이 되어 f는 단사다. 그러나 B에서 A로 가는 함수는 존재할 수 없다. 공역 {1}의 원소 1을 공집합 A의 어떤 원소로도 보낼 수 없기 때문이다. 결국 단사이면서도 좌역원이 없는 함수가 성립하고, "필요충분" 명제의 한 방향이 깨진다.

흥미로운 대목은 저자가 이 반례를 처음부터 논리적으로 떠올린 것이 아니라는 점이다. Rocq에서 명제를 증명하려 할 때마다 벽에 부딪혔고, 자신이 시도한 모든 증명 경로가 하나같이 "A에 원소가 있다" 또는 "B가 비어 있다"는 전제를 요구했다. 한참을 헤맨 끝에 비로소 명제 자체가 참이 아닐 수 있다는 의심에 도달했다. 도구가 사람의 직관이 얼버무리고 넘어가던 전제를 계속 요구하면서, 숨어 있던 가정을 표면으로 끌어올린 셈이다.

형식 검증이 잡아내는 것

이 일화는 소프트웨어 실무자에게도 시사하는 바가 있다. 종이 위의 증명이든 코드든, 사람은 "일반적인" 경우를 머릿속에 그리며 논리를 전개하는 데 익숙하다. 그 과정에서 빈 컬렉션, 널 값, 원소가 없는 상태 같은 경계 조건은 자연스럽게 시야에서 사라진다. 공허한 참(vacuous truth)이란 개념이 대표적이다. 조건을 만족할 대상이 아예 없을 때 그 조건은 자동으로 참이 되는데, 이는 순회 대상이 비어 있는 반복문이나 원소가 없는 배열에 대한 검증 로직에서 실무자가 흔히 놓치는 함정과 정확히 같은 구조다.

증명 보조기는 바로 이 지점에서 위력을 발휘한다. 사람이 무의식적으로 깔고 들어가는 전제를 기계는 봐주지 않기 때문이다. 증명이 특정 가정 없이는 진행되지 않는다면, 그것은 도구의 결함이 아니라 원래 명제가 그 가정을 필요로 한다는 신호다. 단위 테스트가 통과하는 것과 명세가 모든 입력에서 성립함을 증명하는 것은 전혀 다른 층위의 보증이며, 형식 검증은 후자를 지향한다. 항공, 암호, 컴파일러처럼 오류 비용이 큰 영역에서 이런 도구가 쓰이는 이유이기도 하다.

다만 이 사례를 과대 해석하지는 말아야 한다. 문제의 명제는 함수와 집합에 대한 특정 정의를 전제로 할 때만 반례가 성립한다. 실제로 많은 교재나 강의에서는 공집합을 정의역으로 하는 경우를 암묵적으로 배제하거나, 좌역원의 존재를 정의역이 비어 있지 않다는 단서와 함께 다룬다. 저자 스스로도 글을 쓰던 중 책의 정오표(errata)를 확인했더니 이 오류가 이미 등재되어 있었다고 덧붙였다. 즉 알려지지 않은 새로운 발견이라기보다, 형식화라는 과정이 어떻게 미묘한 경계 조건을 스스로 드러내는지를 보여주는 교육적 일화에 가깝다.

그럼에도 실무적 교훈은 분명하다. 명세를 엄밀하게 적어 내려가는 행위 자체가 검증이다. 요구사항을 코드나 형식 언어로 옮기다 보면 원문에서는 모호하게 넘어갔던 가정들이 강제로 명시되고, 그 과정에서 원래 진술의 허점이 드러난다. 반드시 Rocq 같은 전용 도구를 쓰지 않더라도, 경계 조건을 먼저 나열하고 "입력이 없을 때"와 "대상이 비어 있을 때"를 명시적으로 질문하는 습관만으로도 상당수의 결함을 설계 단계에서 걸러낼 수 있다. 권위 있는 교과서조차 예외가 아니라는 사실이야말로, 검증을 사람의 직관에만 맡기지 말아야 할 이유다.