💻 computer science

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

본 논문은 큐비컬 아그다에서 코시 실수의 호모토피 타입 이론 구성을 형식화하여 제시하며, 이 접근법이 다른 구성적 정의에 내재된 가산 선택, 세토이드 오버헤드, 그리고 우주 레벨 추적 문제를 회피하면서도 공리 없이 타입 체킹이 가능함을 보여준다.

원저자: Jackson Brough

게시일 2026-04-29

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Jackson Brough

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

우주에 있는 모든 것을 측정할 수 있는 완벽하고 무한한 자를 만들려고 한다고 상상해 보세요. 고전 수학의 세계에서는 이 자를 설명하기가 쉽습니다. 모든 가능한 '근사' 측정값 (3.1, 3.14, 3.141 등) 을 취하고, "두 측정값 수열이 서로 점점 더 가까워지면, 그들은 자 위의 같은 점을 나타낸다"고 말하기만 하면 됩니다.

그러나 구성주의 수학—즉, 논의하는 대상을 실제로 '구축'하거나 '계산'할 수 있어야 한다고 고집하는 수학 스타일에서는 이 간단한 접근법이 벽에 부딪힙니다. 자의 완비성을 증명하려면, 최종 점을 나타내기 위해 무한한 옵션 목록 중 하나의 특정 측정값을 선택하는 마법 같은 선택을 해야 합니다. 구성주의 수학은 "마법은 허용되지 않습니다. 어떻게 선택했는지 보여줄 수 없다면, 당신은 아직 자를 구축한 것이 아닙니다"라고 말합니다.

수십 년 동안 수학자들은 타협해야 했습니다. 그들은 계산을 번거롭게 만드는 '장부 관리' 트릭을 사용하거나, 복잡한 '우주 수준' (상자의 크기를 점수처럼 추적하는 것) 을 추적해야 하는 방식으로 자를 구축했습니다.

새로운 청사진 (HoTT Book Reals)
이 논문은 유명한 동형 유형 이론 (HoTT) 책에서 가져온 자를 구축하는 새로운 청사진을 제시합니다. 조각들을 붙이고 나서 그들을 매끄럽게 만드는 방식으로 자를 구축하는 대신, 이 방법은 자와 '매끄러움' 규칙을 동시에 구축합니다.

벽과 청사진이 정확히 같은 시간에 그려지는 집을 짓는다고 생각해보세요.

벽돌: 분수처럼 간단하고 알려진 숫자로 시작합니다.
접착제: "두 점이 충분히 가까우면, 실제로는 같은 점이다"라고 말하는 특별한 규칙을 추가합니다.
마법: '가까움' 규칙이 집 자체의 정의에 내장되어 있기 때문에, 나중에 그런 마법 같은 선택을 할 필요가 없습니다. 벽돌을 놓는 순간 집은 완성됩니다.

도전 과제: 컴퓨터 번역기
저자 잭슨 브로는 이 이론적 청사진을 컴퓨터가 이해하고 검증할 수 있는 언어인 Cubical Agda로 번역하려고 시도했습니다.

엄격하고 문자 그대로의 명령만 이해하는 로봇에게 복잡한 춤 동작을 설명하려고 한다고 상상해보세요.

문제: 이 청사진을 번역하려는 이전 시도들은 컴퓨터 언어에 올바른 '동작'이 없었기 때문에 실패했습니다 (특히, 자와 가까움 규칙의 동시 정의를 처리할 수 없었습니다). 번역자들은 "이 동작이 존재한다고 가정하세요"라고 말해야 했는데, 이는 수학에서 속임수입니다.
해결책: Cubical Agda 는 이러한 복잡한 동작을 '네이티브'로 이해하는 더 새롭고 똑똑한 로봇입니다. 이를 통해 저자는 속임수 없이 설계된 그대로 청사진을 작성할 수 있었습니다.

번역 중에 일어난 일
이 논문은 단순히 코드를 타이핑하는 것에 관한 것이 아니라, 저자가 컴퓨터에게 수학을 이해시키려고 시도했을 때 일어난 일에 관한 것입니다. 컴퓨터의 엄격함은 저자로 하여금 원래 설명에 숨겨진 간극을 찾게 했습니다.

"대안" 지도: 원래 책은 두 점이 가까운지 확인하는 방법을 설명했습니다. 그러나 저자가 코드를 작성하려고 시도했을 때, 책의 방법은 '일방통행'과 같다는 것을 깨달았습니다. 점들이 가깝다는 것을 증명할 수는 있지만, 왜 그런지 역으로 쉽게 파악할 수는 없었습니다. 저자는 컴퓨터가 실제로 답을 계산할 수 있도록 역기어 역할을 하는 두 번째 '계산적' 지도 (대안 관계라고 함) 를 구축해야 했습니다.
누락된 재료: 책은 컴퓨터가 원래 근사치 목록을 '기억'할 수 있는 것처럼 함수 (곱셈 등) 를 구축하는 규칙을 설명했습니다. 저자의 첫 번째 코드 버전은 이 기억을 잊어버렸습니다. 컴퓨터는 이를 거부했습니다. 저자는 원래 텍스트가 기계에게는 너무 모호했다는 것을 깨닫고, 기억을 명시적으로 전달하도록 규칙을 다시 작성해야 했습니다.
다변수 퍼즐: 책은 단일 숫자에 대한 규칙이 숫자의 쌍이나 세 쌍에 쉽게 적용될 수 있다고 암시했습니다. 컴퓨터는 이를 납득하지 못했습니다. 저자는 규칙이 한 변수에 대해 작동하면, 하나씩 확인하는 조건 하에 두 변수에 대해서도 작동한다는 것을 보여주는 새로운 특정 보조정리를 증명해야 했습니다.

결과
최종 제품은 HoTT 책의 실수가 완벽하게 작동함을 증명하는 13,000 줄 이상의 방대한 오픈 소스 코드 라이브러리입니다.

이 숫자들이 완전한 순서체 (덧셈, 뺄셈, 곱셈, 나눗셈, 비교가 가능함) 를 형성함을 증명합니다.
자가 '아르키메데스적'임을 증명합니다 (즉, 아무리 작은 간격이 있더라도 그 안에 들어맞는 분수를 항상 찾을 수 있다는 의미입니다).
가장 중요한 것은, 속임수 없이 모든 것을 수행한다는 점입니다. 컴퓨터는 모든 단계를 검증했으며, 코드는 어떤 '마법적인 가정' 없이도 실행됩니다.

요약
이 논문은 아름답고 고차원적인 수학 아이디어를 가져와 컴퓨터 검증의 엄격하고 문자 그대로의 세계에서 생존하도록 만든 이야기입니다. 그렇게 함으로써 저자는 단순히 디지털 자를 구축한 것이 아니라, 청사진 자체를 연마하여 숨겨진 세부 사항을 드러냈고, 이론을 이전보다 더 강력하고 정밀하게 만들었습니다. 이 코드는 이제 미래의 수학 발견을 위한 견고한 기초로 누구나 사용할 수 있습니다.

잭슨 브로우 (Jackson Brough) 의 논문 "Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda"에 대한 상세한 기술적 요약입니다.

1. 문제 제기

구성적 수학 (Constructive mathematics) 은 수학 증명에 계산적 해석을 제공하려 하지만, 실수 ( $\mathbb{R}$ ) 의 구성은 역사적으로 상당한 타협을 요구해 왔습니다:

고전적 코시 구성 (Classical Cauchy Construction): 코시 완비성을 증명하기 위해 코시 수열의 동치류에서 대표원을 선택하기 위해 **가산 선택 공리 (Axiom of Countable Choice)**가 필요합니다. 이는 비구성적입니다.
비숍의 세토이드 구성 (Bishop's Setoid Construction): 명시적 동치 관계 (세토이드) 를 갖춘 코시 수열로 작업함으로써 선택을 피합니다. 그러나 이는 지속적인 **부기 오버헤드 (bookkeeping overhead)**를 도입하여, 모든 연산과 정리에 대해 명시적인 합동성 (congruence) 증명을 요구하므로 대수적 구조를 복잡하게 만듭니다.
데데킨트 절단 (Dedekind Cuts): 예측적 형식 이론 (predicative type theory) 에서 데데킨트 절단은 **우주 수준 (universe levels)**을 추적해야 합니다 (실수는 그 절단보다 한 수준 위에 존재함). 이로 인해 개발이 번거로워집니다.

HoTT Book(Homotopy Type Theory)은 **고차 유도 - 유도형 (Higher Inductive-Inductive Type, HIIT)**으로 실수를 정의함으로써 해결책을 제시합니다. 이 구성은 선택을 피하고, 경로 생성자 (path constructors) 를 통해 $\epsilon$ -근접한 실수를 동일시함으로써 세토이드 오버헤드를 제거하며, 우주 수준 추적을 피합니다. 그러나 이전의 공식화 (예: Rocq 에서 길버트 (Gilbert) 의 작업) 는 증명 보조도구들이 HIIT 를 네이티브로 지원하지 못했기 때문에 불완전했습니다. 이로 인해 저자는 경로 생성자와 그 계산 규칙을 유도하는 대신 **가정 (postulate)**해야 했습니다.

2. 방법론

이 논문은 큐비컬 아그다 (Cubical Agda, 큐비컬 형식 이론 기반의 증명 보조도구) 를 사용하여 HoTT Book 의 실수에 대한 완전한 기계 검증 공식화를 제시합니다.

네이티브 지원: 큐비컬 아그다는 고차 유도형 (HITs) 과 유도 - 유도 정의 (Inductive-Inductive definitions) 를 네이티브로 지원합니다. 이를 통해 저자는 가설 없이 실수와 근접 관계를 동시에 정의할 수 있으며, 경로 생성자가 네이티브 계산 규칙을 갖도록 보장합니다.
공식화 범위: 이 작업은 13,000 줄 이상의 코드를 공식화하며 다음을 포함합니다:
1. $\mathbb{R}$ 의 HIIT 정의와 근접 관계 ( $\sim_\epsilon$ ).
2. 유도 및 재귀 원리.
3. 근접 관계의 성질 (반사성, 대칭성, 삼각 부등식, 반올림성).
4. 리프시츠 (Lipschitz) 및 비확장 사상에 대한 확장 원리.
5. 대수적 연산의 구성 (덧셈, 부호 반전, 최솟값/최댓값, 곱셈, 역수).
6. 순서 이론 (강/비강 부등식, 분리성).
7. $\mathbb{R}$ 이 **아르키메데스 순서체 (Archimedean ordered field)**를 이룬다는 증명.
도구: 저자는 대규모 큐비컬 아그다 표준 라이브러리를 탐색하고 비공식적 증명 스케치를 공식적인 아그다 용어로 변환하는 데 **클로드 코드 (Claude Code, Anthropic 의 AI 에이전트)**를 활용하여 역수 구성과 같은 복잡한 증명 개발을 크게 가속화했습니다.

3. 주요 기여

A. HoTT 실수의 첫 번째 완전한 공식화

이는 가정을 사용하지 않는 최초의 HoTT Book 실수 공식화입니다. 이전 시도들은 경로 생성자의 존재를 가정해야 했지만, 이 작업은 큐비컬 아그다 형식 이론에서 직접 유도하여 모든 계산 규칙이 정의적으로 성립하도록 보장합니다.

B. 공식화 간극의 해결

공식화 과정은 HoTT Book 의 비공식적 제시에서 미묘한 문제들을 드러냈으며, 이는 수학적 정제가 필요했습니다:

대체 근접 관계: 근접성 ( $\sim$ ) 의 유도적 정의는 증명을 추출하기 위한 충분 조건을 제공하지만 필요 조건은 제공하지 않습니다. 공식화는 생성자에서 계산되는 보조 관계 ( $\approx$ ) 를 엄밀하게 구성하고 $\sim \iff \approx$ 를 증명하여 근접성 가정에 대한 경우 분석을 가능하게 합니다.
향상된 재귀 원리: 비공식 텍스트의 재귀 원리 표기는 유도 가정 내에서 도메인 근사 ( $x_\epsilon$ ) 에 대한 접근을 암묵적으로 가정했습니다. 공식화는 근사와 공역 할당을 모두 전달하도록 재귀 원리를 명시적으로 재구성해야 했으며, 이는 초기 단순한 전사 과정에서 간과된 세부 사항이었습니다.
다변수 연속성: HoTT Book 은 별도의 연속성이 다변수에 대한 항등식 확장에 충분함을 시사합니다. 공식화는 이를 명시적으로 증명했습니다 (Lemma 2.3.4). 즉, 별도의 연속성이 $\mathbb{Q}$ 에서 $\mathbb{R}$ 로 이항 및 삼항 항등식을 확장하기에 충분함을 보였습니다.

C. 곱셈과 역수의 구성

곱셈과 역수는 전역적으로 리프시츠가 아니므로 단순한 확장 원리를 통해 정의할 수 없습니다. 논문은 길버트의 국소 - 전역 전략을 채택합니다:

리프시츠 경계가 존재하는 제한된 도메인에서 연산을 정의합니다 (예: 한 인자에 대한 경계 고정).
이러한 국소 정의가 겹침 부분에서 일치함을 증명합니다.
**크라우스 정리 (Kraus's Theorem, 명제 축소에서 집합으로의 사상)**를 사용하여 특정 경계에 대한 의존성을 제거하여 전역 정의를 도출합니다.
이 접근 방식은 큐비컬 아그다 표준 라이브러리의 SetElim 모듈을 사용하여 구현되었습니다.

D. 계산 효율성

Lean 의 고전적 몫 구성 (실수에서 $2+2=4$ 가 정의적으로 성립하지 않음) 과 달리, 큐비컬 아그다의 HoTT 구성은 유리수 입력에 대한 산술이 정의적으로 계산되도록 합니다. 예를 들어, rational(2) + rational(2) = rational(4)는 타입 체커에서 직접 refl(반사성) 로 축소됩니다.

4. 결과

아르키메데스 순서체: 공식화는 구성된 타입 $\mathbb{R}$ 이 0 과 분리된 요소들의 역수 존재를 포함하여 아르키메데스 순서체의 모든 공리를 만족함을 성공적으로 증명합니다.
코드 가용성: 전체 코드베이스 (약 13,500 줄) 는 오픈 소스이며 최신 큐비컬 아그다 표준 라이브러리를 사용하여 구멍이나 가정 없이 타입 검사를 통과합니다.
AI 지원 개발: 논문은 대규모 라이브러리 탐색과 고수준 증명 전략을 저수준 종속 형식 용어로 번역하는 데 LLM 기반 코딩 에이전트를 사용하는 효과성을 입증합니다.

5. 의의

구성적 해석학의 기초: 이 작업은 동등성 기초 (Univalent Foundations) 프로그램 내에서 구성적 해석학을 위한 견고하고 기계 검증된 기초를 제공합니다. 이는 세토이드의 "부기" 부담과 고전적 몫의 "선택" 부담을 제거합니다.
증명 보조도구의 진화: 네이티브 HIT 지원을 결여한 Rocq(Coq) 와 같은 시스템에 비해 HIIT 기반 수학에 큐비컬 아그다가 우월한 환경임을 검증합니다.
향후 작업: 이 공식화는 리만 적분, 미분 방정식과 같은 더 복잡한 구조로 구성적 해석학을 확장하고, **로케이터 (locators, 실수에서 계산을 가능하게 하는 구조)**와 같은 개념을 더 넓은 거리 공간으로 일반화하는 토대를 마련합니다.
방법론적 통찰: 논문은 공식화가 단순한 검증 연습이 아니라, 비공식적 독서만으로는 불가능한 방식으로 암묵적 가정을 드러내고 정리를 정제할 수 있는 수학적 활동임을 강조합니다.

요약하자면, 잭슨 브로우의 논문은 HoTT Book 의 실수에 대한 이론적 우아함과 실용적이고 실행 가능한 수학 사이의 간극을 연결하여, 형식 이론에서 실해석을 위한 검증되고 계산적으로 효율적이며 가정이 없는 기초를 제공합니다.