A formal proof of the Ramanujan--Nagell theorem in Lean 4

이 논문은 Lean 4 와 Mathlib 라이브러리를 활용하여 디오판토스 방정식 $x^2 + 7 = 2^n$의 모든 정수 해를 규명한 라마누잔 - 나겔 정리의 완전한 형식화 증명과 이를 위해 구축된 대수적 수론 기반의 아키텍처 및 증명 전략을 제시합니다.

핵심

🍪 쿠키와 숫자 게임: 문제란 무엇인가?

상상해 보세요. 어떤 마법 같은 쿠키 공장이 있습니다. 이 공장은 $2^n$이라는 숫자만큼의 쿠키를 만듭니다. 여기서 $n$은 1, 2, 3... 같은 자연수입니다.

그런데 이 공장은 이상한 규칙이 하나 있습니다.
"만든 쿠키 수에서 7 개를 빼면, 그 남은 숫자가 반드시 '완벽한 정사각형' 모양 (예: 1, 4, 9, 16...) 으로 쌓여야 한다."

수학자들은 이 규칙을 만족하는 $n$의 값을 찾아냈습니다.

• $n=3$일 때: $2^3 - 7 = 1$ (1 은 $1^2$)
• $n=4$일 때: $2^4 - 7 = 9$ (9 는 $3^2$)
• $n=5, 7, 15$일 때도 마찬가지입니다.

하지만 질문은 이것입니다: "이 외에 다른 $n$ 값은 절대 존재하지 않을까?"
1913 년에 천재 수학자 라마누잔이 이 의문을 제기했고, 1948 년 나겔이 "아니요, 위 5 가지 경우 말고는 절대 없습니다"라고 증명했습니다. 이것이 바로 라마누잔-나겔 정리입니다.

🤖 컴퓨터가 증명을 하다: 왜 이것이 특별한가?

이 논문은 이 증명을 Lean 4라는 '컴퓨터 수학 프로그램'에 입력하여, 컴퓨터가 하나하나 논리를 따져가며 "정말 맞습니다!"라고 확인하게 했습니다.

기존의 수학 증명은 인간이 눈으로 보고 "아, 이건 당연하지"라고 넘어가는 부분이 많았습니다. 하지만 컴퓨터는 "당연한 게 뭐야? 그걸 증명해 봐!"라고 따집니다. 이 논문은 인간이 넘어가던 모든 '당연한 부분'까지 컴퓨터가 납득할 수 있도록 다듬어 넣은 것입니다.

🏗️ 건축가들의 이야기: 증명 과정의 구조

이 증명을 컴퓨터에 입력하는 과정은 마치 고층 빌딩을 짓는 것과 비슷합니다.

1. 기초 공사 (수학 인프라 구축):
   증명을 하려면 먼저 '수학의 땅'을 다져야 합니다. 저자는 $\sqrt{-7}$이라는 이상한 숫자가 들어있는 세계 (수학적으로 '2 차 수체') 를 컴퓨터가 이해할 수 있도록 정의했습니다.

   • 비유: 마치 새로운 나라를 건설할 때, "여기는 땅이 어디까지고, 법은 어떻게 적용되는지"를 컴퓨터에게 일일이 가르치는 작업입니다. 이 부분이 전체 작업의 70% 이상을 차지했습니다.

2. 중요한 발견 (단일성 확인):
   그 나라에서 숫자를 곱하고 나눌 때, '소인수분해'가 항상 유일하게 이루어지는지 확인했습니다. (예: 6 은 2×3 으로만 나뉘지, 다른 방식으로 나뉘지 않는지). 컴퓨터는 이것이 '유일한 소인수분해'가 가능하다는 것을 증명해야만 다음 단계로 갈 수 있었습니다.

3. 마지막 퍼즐 (나머지 분류):
   이제 실제 문제를 풀 차례입니다. 컴퓨터는 $n$이 홀수일 때, $n$을 42 로 나눈 나머지 (나머지 3, 5, 13) 만 가능하다는 것을 증명했습니다. 그리고 이 세 가지 경우 각각에서 해가 하나뿐임을 보였습니다.

   • 비유: "이 나라에 사는 사람 중 나이가 42 로 나눴을 때 3, 5, 13 이 남은 사람만 이 문제를 풀 수 있다"는 것을 증명하고, 그중에서도 정답은 딱 하나뿐임을 확인한 것입니다.

🧱 컴퓨터가 겪은 고충: 인간과 기계의 차이

이 논문은 증명 자체보다 **"왜 컴퓨터로 증명하기가 이렇게 힘들었는지"**에 대한 통찰을 더 많이 줍니다.

• 언어 장벽: 수학자들은 $\sqrt{-7}$을 표현할 때 $\frac{1+\sqrt{-7}}{2}$라는 형태를 쓰지만, 컴퓨터는 이를 $\sqrt{-7}$과 다른 '종류'로 인식합니다. 마치 동일한 사람인데 이름만 다르게 부르면 다른 사람으로 인식하는 것처럼, 컴퓨터는 이 두 가지를 연결해 주는 '번역사 (동형 사상)'를 직접 만들어야 했습니다.
• 당연한 것의 함정: 인간에게는 "이건 당연해, $\sqrt{-7}$이 0 이 아니니까"라고 넘길 수 있는 부분이 컴퓨터에게는 "어떻게 0 이 아님을 증명하지?"라는 거대한 산이 되었습니다.
• AI 의 도움: 이 어려운 작업을 저자는 **인공지능 (AI)**의 도움을 많이 받았습니다. AI 는 "다음 단계는 뭐지?"라고 힌트를 주거나, 코드가 틀렸을 때 "여기 수정해"라고 알려주었습니다. 마치 숙제를 할 때 옆에 앉은 똑똑한 친구가 힌트를 주는 것과 같았습니다. 하지만 최종적인 답은 여전히 컴퓨터 (Lean) 가 검증했습니다.

🌟 결론: 왜 이 일이 중요한가?

이 논문은 단순히 하나의 수학 문제를 푼 것을 넘어, **"미래의 수학은 어떻게 될 것인가?"**를 보여줍니다.

1. 완벽한 신뢰: 인간의 실수나 착각 없이, 컴퓨터가 논리의 모든 고리를 검증했기에 이 결과는 100% 확실합니다.
2. AI 와의 협력: 수학자가 AI 와 함께 복잡한 수학적 구조를 설계하고 검증하는 새로운 방식이 가능해졌습니다.
3. 지식 저장: 이 코드는 앞으로 다른 수학자들이 이 '수학의 땅'을 다시 빌려서 더 복잡한 문제를 풀 수 있는 기초가 됩니다.

결국 이 논문은 **"수학이라는 거대한 성을, 컴퓨터와 AI 가 함께 쌓아 올린 첫 번째 완벽한 청사진"**이라고 할 수 있습니다.

기술 요약

논문 개요

이 논문은 Barinder S. Banwait 에 의해 작성되었으며, Lean 4 상호작용형 정리 증명기 (Interactive Theorem Prover) 와 Mathlib 라이브러리를 사용하여 라마누잔 - 나겔 정리를 완전히 형식화 (Formalization) 한 내용을 담고 있습니다. 이는 람마누잔의 추측을 증명 도구로 처음 검증한 사례이자, 형식적 검증 시스템에서 특정 지수 디오판토스 방정식을 완전히 해결한 첫 번째 사례로 기록됩니다.

1. 문제 정의 (Problem)

• 라마누잔 - 나겔 정리: 디오판토스 방정식 $x^2 + 7 = 2^n$을 만족하는 정수 해 $(n, x)$는 오직 다음 5 가지 경우뿐임을 주장합니다.
  • $(n, x) \in \{(3, \pm1), (4, \pm3), (5, \pm5), (7, \pm11), (15, \pm181)\}$
• 배경: 1913 년 라마누잔이 이 방정식의 해를 찾도록 질문을 던졌고, 1948 년 나겔 (Nagell) 이 이를 증명했습니다. 이 정리는 대수적 수론 입문 과정에서 자주 다루어지지만, 형식적 검증 시스템에서는 아직 구현되지 않았습니다.

2. 방법론 (Methodology)

논문은 표준적인 수학 증명 (Stewart 와 Tall 의 교재 기반) 을 Lean 4 환경에 맞게 재구성하고, 필요한 대수적 수론 인프라를 구축하는 과정을 따릅니다.

• 수학적 접근:

  1. 이차 수체 (Quadratic Field) 설정: $K = \mathbb{Q}(\sqrt{-7})$의 정수환 (Ring of Integers, $\mathcal{O}_K$) 을 고려합니다. $-7 \equiv 1 \pmod 4$이므로 $\mathcal{O}_K = \mathbb{Z}[\frac{1+\sqrt{-7}}{2}]$입니다.
  2. 유일 인수 분해: $\mathcal{O}_K$가 유일 인수 분해 영역 (UFD) 이며, 단위원 (Unit) 이 $\pm 1$뿐임을 이용합니다.
  3. 인수 분해 및 모듈로 연산: 방정식을 $\mathcal{O}_K$에서 인수분해하고, 이항정리 (Binomial Theorem) 를 적용하여 $m = n-2$에 대한 합동식 $-2^{m-1} \equiv m \pmod 7$을 유도합니다.
  4. 경우 분석: $m \pmod{42}$의 세 가지 잉여류 ($3, 5, 13$) 로 축소하고, 각 잉여류당 해가 최대 하나임을 7-adic valuation 을 이용해 증명합니다.

• 형식적 접근 (Lean 4):

  • 인프라 구축: $\mathbb{Q}(\sqrt{-7})$의 정수환, 판별식, 클래스 수 (Class number), 단위원 군 등을 Mathlib 에 구축합니다.
  • 파일 구조: 총 5 개의 파일로 구성되며, 총 3,570 줄의 코드와 125 개의 선언 (정리, 보조정리, 정의) 으로 이루어져 있습니다.
    • QuadraticIntegerROI.lean, RingOfIntegers.lean, FieldIsomorphism.lean: 대수적 수론 인프라 (정수환 식별, 동형사상).
    • Helpers.lean: 판별식, PID 성질, 단위원, 기약성 증명.
    • Basic.lean: 주 증명 로직 (인수분해, mod-42 축소, 유일성 증명).
  • 검증: sorry (미증명 가정) 없이 모든 정리가 Lean 커널에 의해 검증되었으며, 표준 Lean 공리 (propext, Classical.choice, Quot.sound) 만을 의존합니다.

3. 주요 기여 (Key Contributions)

1. 라마누잔 추측의 첫 형식적 증명: 람마누잔의 추측을 증명 도구 (Proof Assistant) 로 검증한 최초의 사례입니다.
2. $\mathbb{Q}(\sqrt{-7})$ 정수환 인프라 구축:
   • 이차 수체의 정수환을 식별하고, 유일 인수 분해 성질을 검증하는 재사용 가능한 라이브러리를 제공합니다.
   • 다른 표현 방식 (예: $\sqrt{-7}$ 생성자 vs $\frac{1+\sqrt{-7}}{2}$ 생성자) 간의 동형사상과 정수 폐포 (Integral Closure) 성질의 이동을 구현했습니다.
3. 교과서 증명과 형식적 증명의 간극 분석:
   • 수학적으로 자명하다고 간주되는 단계 (예: 단위원 군 결정, 정수환 내 산술) 가 형식화 과정에서 얼마나 많은 추가 작업이 필요한지 분석했습니다.
4. AI 보조 도구의 활용:
   • Claude Code 와 Aristotle 같은 생성형 AI 도구를 사용하여 전술 (Tactic) 제안, 증명 복구, 보조정리 발견, 보일러플레이트 생성 등을 수행하여 형식화 효율을 극대화했습니다.

4. 결과 및 기술적 도전 과제 (Results & Challenges)

• 결과: 모든 의존성 (정수환 식별, 클래스 수 1, 단위원 군 등) 을 포함한 완전한 형식적 증명을 성공적으로 완성했습니다.
• 주요 도전 과제:
  1. 정수 폐포와 환 동형사상: 같은 수체를 다른 생성자로 표현할 때 (예: $\omega^2 = -7$ vs $\omega^2 = -2+\omega$), Lean 의 타입 시스템상 다른 타입이 되므로 명시적인 $\mathbb{Q}$-대수 동형사상을 구성하고 정수 폐포 성질을 이동시켜야 했습니다.
  2. 타입 클래스 다이아몬드 (Typeclass Diamonds): QuadraticAlgebra 구조와 DivisionRing 구조에서 파생된 Algebra 인스턴스 간의 충돌을 해결하기 위해 명시적인 인스턴스 선언이 필요했습니다.
  3. 단위원 군 결정: 교과서에서는 Dirichlet 단위 정리를 인용해 간단히 처리하지만, 형식화에서는 totient 경계 계산과 3, 4, 6 차 근의 존재 여부를 정수 방정식으로 풀어 제거하는 과정 (약 70 줄씩) 이 필요하여 계산량이 많았습니다.
  4. $\mathcal{O}_K$ 내 산술: 정수 $\mathbb{Z}$에서는 linarith로 해결되는 문제들이 정수환 $\mathcal{O}_K$에서는 명시적인 강제 변환 (Coercion) 과 재작성 (Rewriting) 을 통해 증명해야 했습니다.
  5. 이항 전개 및 7-adic valuation: mod-42 축소와 유일성 증명 (Uniqueness argument) 을 위해 복잡한 합 (Sum) 재인덱싱과 7-adic valuation 논리가 필요하여 증명 길이가 길어졌습니다.

5. 의의 (Significance)

• 대수적 수론 형식화의 이정표: 이 프로젝트는 대수적 수론의 복잡한 개념 (정수환, 클래스 수, 단위 정리 등) 을 Lean 4 에 성공적으로 통합했음을 보여줍니다.
• AI 와 형식적 검증의 융합: 생성형 AI 도구가 형식적 증명 과정에서 '전술 제안', '오류 수정', '보조정리 탐색' 등을 통해 인간 연구자의 생산성을 획기적으로 높일 수 있음을 실증했습니다.
• 확장성: 구축된 인프라는 다른 이차 수체 (Quadratic Fields) 로 쉽게 일반화될 수 있어, 향후 더 복잡한 디오판토스 방정식이나 수론적 정리의 형식화에 기여할 것으로 기대됩니다.

이 논문은 수학적 증명의 엄밀성을 기계가 검증할 수 있도록 하는 동시에, AI 도구를 활용한 현대적 형식화 방법론의 가능성을 제시한다는 점에서 중요한 의미를 가집니다.