A formalization of the Gelfond-Schneider theorem

이 논문은 리안 4 (Lean 4) 증명 보조도구를 사용하여 힐베르트의 제 7 문제와 그 해법인 겔폰드 - 슈나이더 (Gelfond-Schneider) 정리를 형식화 (formalization) 한 내용을 다룹니다. 저자 미하일 카라타라키스 (Michail Karatarakis) 와 프리크 비디크 (Freek Wiedijk) 는 대수적 수론과 복소해석학의 교차점에 있는 이 심오한 정리를 기계적으로 검증하는 첫 번째 사례를 제시했습니다.

다음은 논문의 기술적 요약입니다.

1. 문제 정의 (Problem)

• 겔폰드 - 슈나이더 정리: $\alpha$와 $\beta$가 대수적 수이고, $\alpha \neq 0, 1$이며 $\beta$가 무리수일 때, $\alpha^\beta$는 초월수 (transcendental number) 임을 증명하는 것입니다.
• 배경: 이 정리는 1934 년 알렉산더 겔폰드와 테오도르 슈나이더에 의해 독립적으로 증명되었으며, 힐베르트의 제 7 문제 (예: $2^{\sqrt{2}}$의 초월성) 를 해결했습니다.
• 과제: 기존 증명 보조도구 (Proof Assistants) 에서는 리우빌 수의 초월성이나 $e, \pi$의 초월성 (리만 - 바이어슈트라스 정리 등) 은 형식화되었으나, 겔폰드 - 슈나이더 정리의 형식화는 이루어지지 않았습니다. 이는 대수적 수론의 깊은 결과와 복소해석학의 정교한 기법 (보조 함수, 성장 추정 등) 을 모두 다루어야 하기 때문입니다.

2. 방법론 (Methodology)

저자들은 리안 4 의 mathlib 라이브러리를 기반으로 대수적 수론과 복소해석학의 도구를 구축하여 증명을 수행했습니다.

가. 대수적 수론 기반 (Algebraic Number Theory)

• 대수적 수의 하우스 (House of an Algebraic Number): 대수적 정수 $\alpha$의 크기를 측정하기 위해 켤레 (conjugates) 의 절대값 중 최댓값인 '하우스'를 정의했습니다. 기존 다항식 근의 집합 접근법 대신, mathlib의 노름 공간 (normed space) API 를 활용하여 표준 매장 (canonical embedding) 을 통해 하우스를 정의함으로써, 삼각부등식과 곱셈 성질 등의 증명을 간소화했습니다.
• 수체 (Number Field) 에 대한 시겔 보조정리 (Siegel's Lemma): 대수적 정수 계수를 가진 선형 연립방정식에서 '작은' 해의 존재를 보장하는 시겔 보조정리를 일반화하여 형식화했습니다. 이는 정수 ($\mathbb{Z}$) 에 대한 기존 시겔 보조정리를 대수적 정수환 ($\mathcal{O}_K$) 으로 확장하기 위해 선형 시스템을 정수 시스템으로 변환 (descent argument) 하는 과정을 통해 구현되었습니다.

나. 분석적 기법 (Analytic Core)

• 보조 함수 (Auxiliary Function) $R(z)$: 특정 점에서 고차로 소멸 (vanish) 하는 보조 함수 $R(z)$를 구성합니다. 시겔 보조정리를 사용하여 $R(z)$의 계수 (대수적 정수) 가 존재하고 그 크기가 제한됨을 증명합니다.
• 전역 보조 함수 $S(z)$ 의 구성: 증명의 핵심 난제 중 하나는 $R(z)$를 $(z-\ell_0)^r$로 나눈 형태인 $S(z)$를 정의하는 것이었습니다. 고전적 증명에서는 유리형 함수 (meromorphic function) 로 간주하지만, 리안에서는 정의역의 부분성 (partiality) 을 피하기 위해 전체 함수 (total function) 로 재구성했습니다.
  • 특이점 (정수 점) 에서 제거 가능한 특이점 (removable singularity) 을 처리하기 위해, 국소적으로 해석적인 함수를 정의하고 이를 조각별로 (piecewise) 연결하여 전역적으로 해석적인 함수를 구성했습니다.
• 모순 유도:
  1. 대수적 하한 (Arithmetic Lower Bound): $\rho = (\log \alpha)^{-r} R^{(r)}(\ell_0)$가 0 이 아닌 대수적 정수임을 이용해, 그 노름 (norm) 의 하한을 유도합니다.
  2. 해석적 상한 (Analytic Upper Bound): 코시 적분 공식 (Cauchy's integral formula) 을 사용하여 $S(z)$의 크기를 추정하고, 이를 통해 $\rho$의 크기가 매우 작아짐을 보입니다.
  3. 결론: 매개변수 $r$을 충분히 크게 잡았을 때, 대수적 하한이 해석적 상한을 초과하여 모순이 발생함을 증명합니다.

3. 주요 기여 (Key Contributions)

• 첫 번째 형식화: 어떤 증명 보조도구에서도 최초로 겔폰드 - 슈나이더 정리를 완전히 형식화했습니다.
• mathlib 확장: 대수적 수론 (하우스, 시겔 보조정리 일반화) 과 복소해석학 (제거 가능한 특이점을 가진 전역 함수 구성, 정교한 성장 추정) 에 대한 새로운 도구와 정리를 mathlib 라이브러리에 통합했습니다.
• 구체적 상수 추적: 고전적 증명에서 $O(\cdot)$ 표기법으로 생략되던 상수들을 $c_1$부터 $c_{15}$까지 명시적으로 정의하고 추적하여, 최종 모순을 유도하는 정량적 논증을 완성했습니다.
• 코드 공개: 프로젝트 코드는 공개되어 있으며, 일부는 이미 mathlib에 통합되었습니다.

4. 결과 (Results)

• 정리 증명: $\alpha \neq 0, 1$인 대수적 수와 무리수인 대수적 수 $\beta$에 대해 $\alpha^\beta$가 초월수임을 성공적으로 증명했습니다.
• 응용: 형식화된 정리를 통해 겔폰드 - 슈나이더 상수인 $\sqrt{2}^{\sqrt{2}}$가 초월수임을 유도하여 증명의 타당성을 검증했습니다.

5. 의의 및 향후 전망 (Significance)

• 수학 형식화의 이정표: 초월수론과 같은 심오한 수학 분야를 기계적으로 검증하는 데 있어 중요한 이정표가 되었습니다.
• 확장 가능성:
  • 베이커의 정리 (Baker's Theorem): 로그의 선형형에 대한 베이커의 정리로 일반화할 수 있는 기반을 마련했습니다.
  • p-진 수론: 복소 해석학 대신 p-진 해석학을 적용하여 p-진 겔폰드 - 슈나이더 정리를 형식화할 수 있습니다.
  • 타원곡선: 지수 함수를 웨어스트라스 $\wp$-함수로 대체하여 타원곡선 관련 초월성 정리 (슈나이더 - 랭 정리 등) 로 확장 가능합니다.
  • 결정 절차 (Decision Procedures): 명시적으로 유도된 상수들을 활용하여 특정 클래스의 초월수에 대한 결정 절차를 구현하거나, 산술적 범위를 이용한 자동화된 검증이 가능해집니다.
  • 샹넬 추측 (Schanuel's Conjecture): 이 작업은 아직 증명되지 않은 샹넬 추측의 결과들을 검증하는 데 필요한 신뢰할 수 있는 기반을 제공합니다.

요약하자면, 이 논문은 대수적 수론과 복소해석학의 복잡한 상호작용을 정밀하게 형식화하여, 수학의 핵심 정리 중 하나를 컴퓨터로 검증하는 새로운 지평을 열었습니다.