A formalization of Borel determinacy in Lean

이 논문은 Lean 4 정리 증명기를 사용하여 게일-스튜어트 게임을 정의하고 마틴의 '순수 귀납적 증명'을 따라 보렐 결정성을 증명하는 형식화를 제시합니다.

핵심

이 논문은 **"무한한 게임에서 누가 이길지 미리 알 수 있을까?"**라는 아주 추상적이고 어려운 수학 문제를, 컴퓨터가 직접 증명할 수 있도록 코드로 작성한 이야기입니다.

수학자 스벤 만테 (Sven Manthe) 는 '린 (Lean)'이라는 컴퓨터 프로그램 언어를 이용해, 1975 년에 마틴 (Martin) 이 증명한 **'보렐 결정성 (Borel Determinacy)'**이라는 거대한 수학 정리를 컴퓨터가 검증하도록 만들었습니다.

이 복잡한 내용을 일상적인 비유로 쉽게 풀어보겠습니다.

---

1. 게임의 세계: 두 명의 플레이어와 무한한 길

이론의 배경이 되는 것은 **'게일 - 스튜어트 게임 (Gale-Stewart game)'**이라는 가상의 게임입니다.

• 상황: 두 사람 (0 번과 1 번) 이 번갈아 가며 숫자나 기호를 하나씩 선택합니다.
• 규칙: 이 선택은 계속 이어져서 무한히 이어집니다.
• 승리 조건: 게임이 끝날 때 (무한히 이어진 후), 만들어진 숫자열이 미리 정해진 '승리 구역 (보렐 집합)'에 들어오면 0 번이 이기고, 아니면 1 번이 이깁니다.

핵심 질문: "이 게임에서 무조건 이기는 '완벽한 전략'이 항상 존재할까?"
수학자들은 "네, 존재합니다"라고 말하지만, 그걸 증명하는 건 매우 어렵습니다. 특히 게임의 규칙이 복잡해질수록 (보렐 집합처럼) 증명하기가 하늘의 별따기 수준입니다.

2. 마틴의 마법: "게임의 규칙을 바꾸는 거울"

이 논문의 주인공인 마틴은 이 난제를 해결하기 위해 아주 영리한 방법을 썼습니다. 바로 **'게임의 거울'**을 만드는 것입니다.

• 비유: 원래의 게임이 미로처럼 복잡하고 헷갈린다고 칩시다. 마틴은 그 미로의 입구를 다른 곳으로 옮겨서, **정말 단순하고 깔끔한 미로 (닫힌 게임)**로 바꾸는 방법을 고안했습니다.
• 원리: 복잡한 게임 (A) 을 거울 (덮개, Covering) 을 통해 단순한 게임 (B) 으로 옮겼을 때, B 에서 이기는 전략을 알면, 그걸로 A 에서도 이기는 전략을 만들 수 있다는 것입니다.
• 결과: 단순한 게임은 이기는 전략이 있다는 게 이미 증명되어 있으므로, 복잡한 게임도 결국 이기는 전략이 있다는 결론에 도달합니다.

3. 컴퓨터가 해낸 일: "수학자의 머릿속을 코드로 옮기다"

이 논문은 마틴의 이 증명 과정을 컴퓨터 언어 (린 4) 로 완벽하게 번역했습니다. 여기서 몇 가지 재미있는 시도가 있었습니다.

A. "불완전한 함수"를 어떻게 다룰까? (쓰레기 값 vs 조건부)

컴퓨터 프로그래밍에서는 함수가 입력값이 없을 때 어떻게 해야 할지 고민합니다.

• 기존 방식 (쓰레기 값): 입력이 없으면 "0"이나 "null" 같은 가짜 값을 줍니다. (예: "나이가 없으면 0 세로 처리")
• 이 논문의 방식 (조건부): 입력이 없으면 "함수 자체가 성립하지 않는다"고 엄격하게 정의합니다. (예: "나이가 있는 사람만 이 함수를 쓸 수 있음")

저자는 **"수학자들은 원래 조건부 방식을 쓰는데, 컴퓨터가 그걸 따라오게 만들자"**고 했습니다. 마치 "빈 그릇에 물이 없으면 '물 없음'이라고 표시하는 게 아니라, '물이 있는 그릇만 이 수저로 떠낼 수 있다'고 규정하는 것"과 같습니다. 이 방식이 증명 과정에서 훨씬 논리적이고 깔끔했습니다.

B. "게임의 레벨"을 맞추는 작업

게임이 무한히 이어지다 보니, 컴퓨터가 모든 경우의 수를 다 따지려면 머리가 터집니다.

• 저자는 게임을 **레벨 1, 레벨 2, 레벨 3...**으로 나누어, 각 단계마다 규칙이 어떻게 변하는지 추적했습니다.
• 마치 레고 블록을 쌓아 올릴 때, 아래쪽 블록이 흔들리지 않도록 위쪽 블록을 딱 맞게 조립하듯이, 무한한 게임의 구조를 단계별로 고정시켜 컴퓨터가 혼란스러워하지 않게 만들었습니다.

4. 왜 이 일이 중요한가?

• 컴퓨터의 한계 돌파: 보통 컴퓨터는 아주 단순한 수학 문제만 풀 수 있습니다. 하지만 이 논문은 "무한"과 "복잡한 규칙"이 섞인 고급 수학 문제를 컴퓨터가 직접 검증하게 했습니다.
• 미래의 신호: 이 기술이 발전하면, 앞으로 더 복잡한 수학 정리나 심지어 물리학의 난제들도 컴퓨터가 "틀림없음"을 확인해 줄 날이 올지도 모릅니다.
• 코드의 품질: 저자는 "컴퓨터가 수학자를 대신할 때, 수학자의 원래 사고방식 (조건부) 을 그대로 존중해 주는 게 더 좋다"는 새로운 기준을 제시했습니다.

요약

이 논문은 **"복잡하고 끝없는 게임에서도 항상 이기는 방법이 있다"**는 수학의 위대한 정리를, 컴퓨터가 직접 코드로 작성하고 검증해낸 성과입니다. 마치 미로 찾기 게임의 지도를 컴퓨터가 직접 그려서 "여기서 이 길로 가면 무조건 출구다"라고 확신 있게 알려주는 것과 같습니다.

이 작업은 수학의 정밀함과 컴퓨터의 논리가 만나, 인간이 혼자서는 하기 힘들었던 거대한 증명을 성공적으로 완성했다는 점에서 매우 의미 있습니다.

기술 요약

1. 문제 제기 (Problem)

• 배경: Gale-Stewart 게임 (무한 두 플레이어 게임) 의 결정성 (Determinacy) 은 기술적 집합론의 핵심 주제입니다. 보렐 집합 (Borel sets) 에 대한 결정성은 ZFC (선택 공리를 포함한 체르멜로 - 프렝켈 집합론) 내에서 증명 가능하지만, 그 증명 과정은 매우 복잡하고 강력한 논리적 힘을 요구합니다.
• 과제: 기존에 닫힌 집합 (Closed sets) 에 대한 결정성은 증명 도구에서 공식화되었으나, 그 이상의 보렐 집합에 대한 결정성은 증명 도구에서 공식화된 바가 없었습니다.
• 도전 과제:
  • Martin 의 증명은 순서수 (Ordinals) 에 대한超限歸納 (Transfinite Induction) 과 복잡한 역극한 (Inverse Limit) 구성을 포함하여 형식화하기 어렵습니다.
  • Lean 의 표준 라이브러리 (mathlib) 는 부분 함수를 구현할 때 '불필요한 값 (junk values, 예: 0 또는 $\bot$)'을 사용하는 방식을 선호하는데, 이는 수학적 직관과 다른 접근 방식입니다.
  • Lean 의 자동화 도구 (Tactics) 가 종속 타입 (Dependent Types) 을 다루는 데 있어 약점을 보이며, 이는 부분 함수를 정의역으로 제한하는 방식 (첫 번째 접근법) 을 사용할 때 성능 저하를 초래할 수 있습니다.

2. 방법론 (Methodology)

논문은 Martin 의 "A purely inductive proof of Borel determinacy" [Mar85] 를 기반으로 하되, 형식화의 효율성을 높이기 위해 다음과 같은 기술적 수정을 가했습니다.

A. 증명 전략의 변형: 보편적 풀림 가능성 (Universal Unravelability)

• 기존 접근: Martin 은 보렐 계층의 순서수에 대한超限歸納을 사용하여 '풀림 가능성 (Unravelability)'을 증명했습니다.
• 본 논문 접근:
  • 보편적 풀림 가능성 (Universal Unravelability) 도입: 단순히 게임이 풀릴 수 있는 것이 아니라, 모든 덮개 (Covering) 하에서 풀릴 수 있는 더 강한 성질을 정의했습니다.
  • $\sigma$-대수 구조 증명: 이 강한 성질이 보렐 집합의 $\sigma$-대수 구조를 이룸을 증명함으로써, 순서수에 대한 명시적인 귀납을 피하고 보렐 집합의 구성 (가산 합집합 등) 에 대한 직접적인 귀납을 가능하게 했습니다.
  • 가산 합집합 처리: Martin 의 역극한 구성을 범주론 (Category Theory) 을 사용하여 일반화했습니다. 특히, $k$-고정 (k-fixing) 사상에 대한 역극한이 계층별로 안정화됨을 범주론적 보조정리를 통해 증명했습니다.

B. 게임 및 전략의 형식화

• 데이터 구조: 유한 시퀀스를 리스트 (List) 로 표현하되, 수학적 표기법과 일치하도록 리스트의 첫 번째 요소를 게임의 첫 수로 매핑했습니다.
• 전략의 정의:
  • Prestrategy (전전략): 위치에서 가능한 이동 집합을 반환하는 함수로 정의했습니다. 이는 '전략 (Strategy)'과 '준전략 (Quasistrategy)'보다 약한 개념으로, 증명 과정에서 더 유연하게 사용되었습니다.
  • 함수적 전략 vs 전략 트리: Martin 은 전략을 '전략 트리'로 정의했으나, Lean 에서는 **함수적 전략 (Functional Strategy)**을 주로 사용했습니다. 이는 재귀 정의를 피하고 특정 전략을 정의하기 쉽기 때문입니다. 다만, 승리 전략의 정의 등 일부에서는 전략 트리를 사용하는 사상 (Surjection) 을 통해 연결했습니다.
• 닫힌 집합의 풀림 (Unraveling of Closed Sets): 닫힌 게임이 풀림 가능함을 증명하기 위해, 플레이어들이 자신의 전략 (또는 준전략) 과 유한 시퀀스를 추가로 플레이하는 새로운 게임을 구성했습니다. 이를 위해 A' := A × Tree A와 같은 곱 타입을 사용하여 이동을 표현했습니다.

C. Lean 특화 기술적 해결

• 부분 함수의 처리: mathlib 의 관례 (불필요한 값 사용) 를 따르지 않고, 정의역을 제한하는 종속 타입 (Dependent Types) 방식을 채택했습니다. 즉, 함수 $f: \{x \mid P(x)\} \to Y$ 형태로 정의하여 수학적 정의에 더 가깝게 만들었습니다.
• 자동화 (Automation) 개선:
  • omega 전략: 플레이어의 위치 (짝수/홀수 길이) 를 판별하는 Presburger 산술 문제를 해결하기 위해 리스트 길이 확장을 수행하는 커스텀 전략을 개발했습니다.
  • Fixing 타입클래스: $k$-고정 사상에 대한 조건을 자동 추론하기 위해 Lean 의 타입클래스 인퍼런스 메커니즘을 활용했습니다.
  • 성능 최적화: 종속 타입을 사용할 때 발생하는 증명 항 (Proof Terms) 의 중첩으로 인한 성능 저하 (지수 시간 복잡도) 를 해결하기 위해, 증명 항을 즉시 보조 정리 (Lemma) 로 추상화하는 메타프로그램 (abstract 및 as_aux_lemma) 을 개발하여 적용했습니다.

3. 주요 기여 (Key Contributions)

1. 최초의 보렐 결정성 공식화: 닫힌 집합을 넘어 보렐 집합에 대한 결정성을 증명 도구에서 공식화한 최초의 사례입니다. 약 5,000 줄의 코드로 이루어진 프로젝트입니다.
2. 범주론적 역극한 구성: Martin 의 역극한 구성을 범주론적 언어로 정교하게 재구성하여, $k$-고정 사상의 성질을 일반화하고 형식화했습니다.
3. 보편적 풀림 가능성의 도입: 순서수 귀납 없이 보렐 결정성을 증명할 수 있도록 '보편적 풀림 가능성' 개념을 도입하고 그 $\sigma$-대수 성질을 증명했습니다.
4. Lean 의 부분 함수 처리 방식에 대한 논의: '불필요한 값' 대신 '정의역 제한' 방식을 사용할 때의 장단점을 실증적으로 분석하고, 종속 타입을 효율적으로 다루기 위한 도구 (메타프로그램) 를 개발했습니다.

4. 결과 (Results)

• 성공적인 증명: Lean 4 와 mathlib 라이브러리를 사용하여 Martin 의 정리를 완전히 증명했습니다.
• 코드 구조:
  • 기초 정의 (게임, 결정성 등) 는 전체 코드의 절반 미만입니다.
  • 대부분의 코드는 Martin 의 증명 과정, 특히 가산 합집합 처리와 닫힌 게임의 풀림 가능성 증명에 할당되었습니다.
• 성능: 메타프로그램을 통한 증명 항 추상화 없이는 형식화 시간이 지수적으로 증가하여 실용적이지 않았으나, 이를 통해 실행 시간을 최적화했습니다.

5. 의의 및 향후 과제 (Significance & Future Work)

• 형식적 수학의 확장: ZFC 보다 강력한 이론 체계 (Lean 의 타입 이론) 에서도 보렐 결정성이 성립함을 보여주었습니다. 이는 큰 카디널 (Large Cardinals) 이 필요한 더 강한 결정성 (Analytic Determinacy) 을 제외한 대부분의 집합론적 명제가 Lean 에서 다루어질 수 있음을 시사합니다.
• 기술적 통찰: Lean 의 simp 및 rewrite 전략이 종속 타입을 다룰 때 겪는 한계와 이를 극복하기 위한 전략 (커스텀 합동성 보조정리, 메타프로그램 등) 을 제시했습니다. 이는 향후 Lean 프로젝트에서 부분 함수를 다룰 때 중요한 가이드라인이 됩니다.
• 향후 연구 방향:
  • 큰 카디널 가정 하에서의 더 넓은 집합 클래스 (예: 해석적 집합) 에 대한 결정성 공식화.
  • 결정성에서 큰 카디널을 갖는 내부 모델 (Inner Models) 을 구성하는 역방향 증명.
  • 기술적 집합론 (Descriptive Set Theory) 에 대한 포괄적인 공식화 라이브러리 구축을 위한 기초 자료 제공.

결론적으로, 이 논문은 고난도 수학 정리의 형식화 과정에서 발생하는 이론적, 기술적 난제를 해결한 모범 사례이며, Lean 을 활용한 집합론 연구의 새로운 지평을 열었습니다.