ZFLean: a framework for set-level mathematics in Lean

비트린 트레라의 논문 "ZFLean: Lean 에서의 집합 수준 수학을 위한 프레임워크"에 대한 상세한 기술적 요약입니다.

1. 문제 제기

Lean 과 같은 증명 보조기에서의 현대적 형식화는 주로 타입 이론(특히 종속 타입 이론)에 기반을 두고 있으며, 여기서 수학적 객체는 구성된 타입으로 표현됩니다. 이 방식은 강력하지만, 종종 선호되는 집합 수준 수학(ZFC)에는 번거로울 수 있습니다. 그 이유는 다음과 같습니다:

• 확장적 추론: 구성이 아닌 원소에 기반한 등가에 대한 추론.
• 부분성: Option 타입이나 종속 타입으로 인코딩하는 대신 관계를 통해 부분 함수를 자연스럽게 처리.
• 범주론적 추론: 엄격한 정의적 등가가 아닌 "동형사상까지" 작업.

도전 과제: 타입이 있는 보조기 (Lean 의 Mathlib ZFC 모델과 같은) 내에서 집합론적 모델을 직접 사용하는 것은 상당한 마찰을 초래합니다:

• 보일러플레이트: 사용자가 "부수 조건"(예: 관계가 잘 정의됨을 증명, 함수가 전체임을 증명) 을 수동으로 계속 관리해야 함.
• 취약성: 집합론적 객체 (ZFSet) 와 네이티브 Lean 타입 (Type) 사이의 경계를 넘나드는 과정이 수동이며 오류가 발생하기 쉬움.
• 자동화 부족: 기존 도구들은 집합론적 증명을 타입 증명만큼 유연하게 만들기 위해 필요한 특정 재작성 힌트와 전술 (tactics) 이 종종 부족함.

2. 방법론

저자는 Mathlib의 기존 ZFC 모델 위에 구축된 Lean 4 라이브러리인 ZFLean을 제시합니다. 방법론은 집합 수준 개발을 인간 친화적으로 만들기 위한 균일한 관계적 미적분과 상호 운용성 브리지 생성에 중점을 둡니다.

핵심 설계 선택:

• 기반: Mathlib의 ZFC 구현을 활용하며, 여기서 집합은 귀납적 "전-집합"(pre-sets, PSet) 의 확장적 몫으로 구성됩니다.
• 관계적 미적분: 표준 타입 이론에서와 같이 함수를 1 등가 총체적 객체로 취급하는 대신, ZFLean 은 이를 함수적 관계로 취급합니다. 이는 이항 관계, 부분 함수, 그리고 총체적 함수를 위한 미적분을 도입합니다.
• 전술을 통한 자동화: 이 프레임워크는 잘 형성된 부수 조건 (예: 합성이 관계나 함수임을 증명) 을 자동으로 해결하도록 설계된 세 가지 경량 전술 (zrel, zpfun, zfun) 을 도입합니다.
• 브리지: 이 라이브러리는 표준 ZFC 객체 (예: ZFBool, ZFNat) 와 Lean 의 네이티브 타입 (Bool, Nat) 사이의 명시적 동형사상 (브리지) 을 구성하여 두 세계 간에 성질을 이동시킬 수 있게 합니다.

3. 주요 기여

A. 관계적 미적분 및 자동화

• 정의: 관계에 대한 역, 항등, 합성, 정의역, 치역, 그리고 상을 형식화합니다.
• 함수성: 부분 함수 (IsPFunc) 와 총체적 함수 (IsFunc) 를 구분합니다.
• 전술:
  • zrel: 집합이 관계임을 증명하는 목표 ($R \subseteq A \times B$) 를 해결합니다.
  • zpfun: 집합이 부분 함수임을 증명하는 목표를 해결합니다.
  • zfun: 집합이 총체적 함수임을 증명하는 목표를 해결합니다.
  • 이러한 전술은 재귀적으로 부수 조건을 해결하기 위해 속성 태그가 달린 보조 정리 (예: @[zfun]) 를 사용하여 사용자에게 보일러플레이트를 숨깁니다.
• 표기법: 함수 적용 (@zf(x)) 과 $\lambda$-추상화를 위한 편리한 구문을 도입하며, $\beta$-축약, $\eta$-확장, 그리고 확장성에 대한 정리를 제공합니다.

B. 표준 구성

이 라이브러리는 보편적 성질을 갖춘 ZFC 내에서 정의된 표준 수학적 객체들의 세트를 제공합니다:

• 부울: 논리곱, 논리합, 부정을 포함하는 대수적 구조와 사례 제거기가 있는 2 원소 집합 $B$.
• 자연수 ($\mathbb{N}$): 가장 작은 귀납적 집합 (폰 노이만 순서수) 으로 정의됨. 재귀자, 귀납 원리, 그리고 산술 연산을 포함합니다. 특히, Lean 의 ring 전술을 활용할 수 있도록 CommSemiring 구조를 갖추고 있습니다.
• 정수 ($\mathbb{Z}$) 와 유리수 ($\mathbb{Q}$): 자연수/정수의 쌍의 몫 타입으로 구성되며, 연산은 대표원으로부터 승격됩니다.
• 코곱과 옵션: 합 타입과 옵션 타입의 집합론적 정의.

C. 동형사상과 이동

• 임베딩과 동형사상: 단사 함수와 전단사 함수를 통해 집합 수준 임베딩 ($A \hookrightarrow_z B$) 과 동형사상 ($A \cong_z B$) 을 정의합니다.
• 칸토어 - 슈뢰더 - 베른슈타인 정리: 프레임워크 내에서 형식화됨.
• 이동: ZFC 구성이 Lean 의 네이티브 타입과 동형임을 증명합니다 (예: ZFBool $\simeq$ Bool). 이를 통해 사용자는 풍부한 Mathlib 타입 이론 라이브러리의 정리를 집합론적 문맥으로 매끄럽게 "이동"할 수 있습니다.

D. 사례 연구: 커링 동형사상

이 논문은 커링 동형사상: $C^{A \times B} \cong (C^B)^A$를 증명함으로써 프레임워크의 유용성을 시연합니다.

• 증명에서는 curryz와 uncurryz를 집합 수준 함수로 정의합니다.
• 프레임워크의 자동화를 사용하여 부수 조건 (합성과 상의 잘 정의됨) 을 처리함으로써 이들이 상호 역함수임을 증명합니다.
• 증명 스크립트는 표준 수학적 논증과 거의 동일하게 작성되며, 자동화 계층이 "지루한" 집합론적 검증을 처리합니다.

4. 결과

• 아티팩트 크기: 라이브러리는 8,324 줄의 Lean 코드와 706 개의 증명된 정리로 구성됩니다.
• 구성 요소 분해:
  • 관계적 미적분: 약 2,534 줄 (172 개 정리).
  • 자연수: 약 1,260 줄 (199 개 정리).
  • 임베딩/동형사상: 약 1,626 줄 (31 개 정리).
• 사용성: 사례 연구는 이 프레임워크가 집합 수준 형식화의 마찰을 성공적으로 줄였음을 보여줍니다. 사용자는 관계의 모든 합성이 유효한 관계임을 수동으로 증명할 필요 없이 표준 집합론적 논증처럼 보이는 증명을 작성할 수 있습니다.
• 상호 운용성: ZFSet과 네이티브 Type 간에 전환할 수 있는 능력은 집합론적 객체에 Mathlib의 대수적 전술 (예: ring) 을 재사용할 수 있게 합니다.

5. 의의

• 기반의 연결: ZFLean 은 단일 증명 보조기 내에서 수학의 "집합론적" 관점과 "타입 이론적" 관점을 효과적으로 조화시킵니다. 이는 수학자들이 특정 문제에 가장 자연스러운 기반 (확장적 집합 대 구성적 타입) 을 선택하면서도 생태계의 자동화 접근성을 잃지 않도록 합니다.
• 인간 친화성: 집합론에 내재된 지루한 부수 조건 (소속 증명, 관계의 잘 정의됨) 을 자동화함으로써, ZFC 개발을 비전문가에게도 실현 가능하게 하고 대규모 형식화에 실용적으로 만듭니다.
• 확장성: 모듈식 설계 (관계적 미적분 + 표준 객체 + 브리지) 는 쉬운 확장을 가능하게 합니다. 향후 작업은 실수 (코시 수열 또는 데데킨트 절단을 통해) 와 기본 해석학의 형식화를 포함합니다.
• 비교: 집합론이 별도의 객체 논리인 Isabelle/ZF나 타입 이론 자동화와 깊은 통합이 종종 부족한 Rocq 의 집합론적 개발과 달리, ZFLean 은 집합 수준에서 증명을 유지하면서 Lean 의 네이티브 타입 이론 인프라를 활용하는 하이브리드 접근법을 제공합니다.

결론적으로, ZFLean 은 Lean 4 내에서 ZFC 로 핵심 수학을 수행하기 위한 강력하고 인간 친화적이며 상호 운용 가능한 프레임워크를 제공하며, 집합론적 형식화의 진입 장벽을 성공적으로 낮추면서도 광범위한 Mathlib 생태계와의 호환성을 유지합니다.