"1/2의 세 번째 좌표는 전단사 함수입니다" - Lean 증명 도구의 기묘한 진실

안녕하세요. 풀링포레스트 백엔드 개발자 김테크입니다.

개발자로서 우리는 '엄밀함'을 사랑합니다. 특히 타입 시스템이 강력한 언어를 다룰 때면, 컴파일러가 잡아주는 오류 덕분에 심리적 안정감을 느끼곤 하죠. 저 역시 최근 백엔드 안정성을 높이기 위해 형식 검증(Formal Verification) 도구인 Lean을 공부하다가, 제 상식을 완전히 무너뜨리는 기묘한 리포지토리 하나를 발견했습니다.

제목부터 심상치 않은 'Some Junk Theorems in Lean'이라는 문서였습니다. 직역하자면 'Lean에서의 잡동사니 정리들' 정도가 되겠네요. 오늘은 제가 이 문서에서 발견한 충격적이고도 재미있는, 그리고 개발자로서 한 번쯤 곱씹어볼 만한 '참(True)이지만 무의미한(Junk)' 정리들에 대해 이야기해보려 합니다.

유리수 1/2의 '좌표'를 찾아서

우리가 아는 수학에서 유리수 1/2은 그냥 숫자입니다. 그런데 Lean이라는 증명 도구 안에서는 다음 정리가 '참'으로 증명됩니다.

정리 1: 유리수 1/2의 세 번째 좌표는 전단사(bijection)이다.

처음 이 문장을 보고 "내가 수학을 잘못 배웠나?" 싶었습니다. 숫자에 무슨 좌표가 있고, 그게 심지어 함수(전단사)라니요? 더 황당한 정리들도 있습니다.

정리 2: 다항식 $X^2(X^3 + X + 1)$의 첫 번째 좌표는 30의 소인수분해와 같다.
정리 6: 다음은 동치이다: 7의 이진 전개(binary expansion).

이게 도대체 무슨 소리일까요? 7의 이진 전개가 동치라니, 문장 자체가 성립이 안 되는 것 같지 않나요? 하지만 Lean의 컴파일러(정확히는 증명 커널)는 이것들이 수학적으로 엄밀하게 '참'이라고 말합니다.

왜 이런 일이 벌어질까: 구현의 누수

이 현상을 이해하려면 우리는 수학자가 아니라 '개발자'의 관점으로 돌아와야 합니다. 우리가 코드를 짤 때 객체나 데이터를 어떻게 모델링하는지 떠올려보세요.

Lean이나 여타 프로그래밍 언어에서 수학적 개념을 구현하려면 결국 '구조체(Structure)'나 '클래스' 같은 데이터 구조로 정의해야 합니다. 예를 들어 유리수 $\mathbb{Q}$를 정의한다고 칩시다. 아마도 이렇게 구현되겠죠.

structure Rational where
  num : Int        -- 분자 (1번 좌표)
  den : Nat        -- 분모 (2번 좌표)
  is_coprime : ... -- 서로소임을 증명하는 증명 객체 (3번 좌표)
  den_nz : ...     -- 분모가 0이 아님을 증명하는 객체 (4번 좌표)

여기서 '1/2'이라는 유리수는 사실 `(1, 2, 증명1, 증명2)`라는 튜플 형태의 데이터 덩어리로 메모리에 존재하게 됩니다. Lean에서 '유리수의 세 번째 좌표'를 꺼내라는 말은, 수학적으로는 말이 안 되지만 구현상으로는 `is_coprime`이라는 필드(증명 객체)를 꺼내라는 아주 명확한 명령이 됩니다.

그리고 Lean에서는 '증명' 자체도 함수나 타입으로 취급되곤 합니다. 우연히 그 내부 구조가 전단사 함수의 정의와 맞아떨어졌다면? 컴퓨터 입장에서는 "네, 타입이 일치하네요. 참입니다."라고 대답할 수밖에 없는 것이죠.

1/0 = 0, 그리고 개발자의 타협

또 다른 흥미로운 사례는 '부분성(Partiality)'에 관한 것입니다. 개발자라면 누구나 두려워하는 `DivisionByZero` 에러가 수학 증명 도구에서는 어떻게 처리될까요?

정리 9: 리만 제타 함수 $\zeta(1) = \frac{1}{2}(\gamma - \log 4 \pi)$

원래 리만 제타 함수는 1에서 정의되지 않습니다(발산합니다). 하지만 Lean을 비롯한 많은 증명 보조 도구는 모든 함수를 '전함수(Total Function)'로 만들기 위해 편의상 $\frac{1}{0} = 0$으로 정의해 버립니다. 입력을 넣으면 무조건 출력이 나와야 프로그램이 터지지 않으니까요. 그 결과, 수학적으로는 정의되지 않는 값에 대해 엉뚱한 수식이 성립한다는 '잡정리'가 튀어나오게 됩니다.

이건 우리가 실무에서 `null` 처리를 하기 싫어서 기본값을 0이나 빈 문자열로 세팅했다가, 나중에 비즈니스 로직에서 0이 '없음'인지 '숫자 0'인지 헷갈려서 버그를 만드는 상황과 소름 돋게 닮아 있습니다.

가장 무서운 이야기: a=b, b=c인데 a!=c?

마지막으로 저를 가장 공포에 떨게 했던 정리는 타입 시스템의 어두운 면을 보여줍니다.

정리 13: a는 b와 같고, b는 c와 같다. 하지만 a와 c가 같은지 묻는 것은 타입 에러다.

이건 마치 TypeScript에서 `any`로 타입을 우회해서 억지로 할당은 했는데, 막상 컴파일러가 "이 두 변수는 비교 자체가 불가능합니다"라고 뱉어내는 상황 같습니다. $a$와 $b$는 호환되는 타입이고, $b$와 $c$도 호환되지만, 정작 $a$와 $c$는 서로 다른 우주에 살고 있어서 비교조차 할 수 없는 상황. Banach 공간이 몬스터 군(Monster group)과 같은지 묻는 것이 넌센스인 것처럼, 시스템 내부적으로 $a$와 $c$는 전혀 다른 타입으로 추론되기 때문에 발생하는 현상입니다.

맺음말: 지도는 영토가 아니다

이 '잡동사니 정리'들을 보면서 저는 역설적으로 안도감을 느꼈습니다. 아무리 완벽해 보이는 논리 시스템이나 프레임워크도 결국은 사람이 만든 '모델'일 뿐이라는 사실을 확인했기 때문입니다.

우리가 현실의 문제를 해결하기 위해 코드를 짤 때, 우리는 필연적으로 현실을 추상화하고 단순화합니다. 그 과정에서 $\frac{1}{0}=0$ 같은 타협을 하기도 하고, 유리수를 구조체로 욱여넣기도 하죠. 중요한 건 그 타협이 만들어내는 '부산물(Side Effect)'을 우리가 인지하고 있느냐는 것입니다.

도구의 특성을 이해하지 못하고 맹목적으로 믿으면, 우리는 "1/2의 세 번째 좌표는 전단사 함수"라는 엉뚱한 결론을 붙들고 씨름하게 될지도 모릅니다. 풀링포레스트 팀원 여러분, 그리고 이 글을 읽으시는 개발자분들도 오늘 내가 작성한 코드가 현실을 올바르게 반영하고 있는지, 아니면 구현상의 편의가 만들어낸 '잡정리'에 속고 있는 건 아닌지 한 번쯤 생각해보는 하루가 되시길 바랍니다.

감사합니다.