💻 computer science

A formalization of the Gelfond-Schneider theorem

この論文は、代数的数 $\alpha$ （0, 1 以外）と無理数 $\beta$ に対して $\alpha^\beta$ が超越数となることを主張するヒルベルトの第 7 問題の解決であるゲルフォン＝シュナイダーの定理を、Lean 4 証明支援系を用いて形式化したものである。

原著者： Michail Karatarakis, Freek Wiedijk

公開日 2026-03-27

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Michail Karatarakis, Freek Wiedijk

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

この論文は、**「数学の証明を、コンピュータが間違いなくチェックできるように書き直す」**という壮大なプロジェクトについて書かれています。

具体的には、100 年前に解決された有名な数学の問題（ヒルベルトの第 7 問題）と、その解決策である**「ゲルフォント・シュナイダーの定理」**を、現代の「Lean（リーン）」という強力な証明支援ソフトウェアを使って、ゼロから再構築しました。

これを一般の方にもわかりやすく、いくつかの比喩を使って説明します。

1. 物語の舞台：数字の「正体」を暴く探偵

まず、この定理が何を言っているのかを理解しましょう。

代数数（Algebraic Numbers）： 整数の係数を持つ方程式の解になる数字です（例： $1/2$ や $\sqrt{2}$ ）。これらは「規則性のある数字」です。
超越数（Transcendental Numbers）： どのような方程式でも解にならない数字です（例： $\pi$ や $e$ ）。これらは「規則性のない、自由奔放な数字」です。

ゲルフォント・シュナイダーの定理は、こんなことを言っています。

「もし、規則性のある数字（代数数） $\alpha$ と $\beta$ を使って、 $\alpha^\beta$ （ $\alpha$ の $\beta$ 乗）という計算をしたとき、 $\alpha$ が 0 や 1 ではなく、 $\beta$ が『分数ではない無理数』なら、その答えは必ず『自由奔放な数字（超越数）』になる」

例えるなら：
「整然とした家（代数数）から出発して、少しだけ不規則な道（無理数）を歩くと、必ず『見知らぬ荒野（超越数）』にたどり着く」というルールです。
例えば、 $2^{\sqrt{2}}$ という数字は、一見すると単純そうに見えますが、実は「超越数」であることがこの定理で保証されます。

2. この論文のすごいところ：コンピュータによる「完全な証明」

昔、数学者たちはこの定理を証明しました。しかし、人間の証明には「ここは省略して」「直感的に明らか」といった部分が含まれることがありました。

この論文の著者たちは、**「人間の直感に頼らず、コンピュータが一つ一つのステップを論理的に追えるように、証明を完全に書き直した」**のです。

Lean（リーン）： これは「厳格な数学の裁判所」のようなものです。ここで証明を提出すると、コンピュータが「ここが飛躍している」「定義が曖昧だ」と即座に指摘します。
結果： この定理が、コンピュータのチェックを 100% 通過して、間違いなく正しいことが確認されました。これは、この分野における歴史的なマイルストーンです。

3. 証明の仕組み：魔法の「補助関数」という罠

この定理を証明するために、数学者たちは非常に巧妙なトリックを使います。論文では、このプロセスを以下のように描いています。

① 罠を仕掛ける（補助関数の作成）

探偵（数学者）は、特定の点で「消える（0 になる）」ように設計された、複雑な関数（補助関数）を作ります。

比喩： 特定の場所（整数の点）にだけ、足跡を残さないように設計された「幽霊のような関数」です。
この関数を作るために、**「シゲルの補題（Siegel's Lemma）」**という道具を使います。これは「小さな数字の組み合わせを見つけ出す魔法の網」のようなもので、複雑な方程式から、条件を満たす小さな解を無理やり引き出します。

② 二つの視点からの攻撃（矛盾の発見）

この「幽霊のような関数」を使って、矛盾を導き出します。

視点 A（代数的な視点）：
この関数の値は「代数数」の組み合わせなので、もし 0 でなければ、ある一定の大きさ（絶対値）以下にはなれないはずです。
- 例：「この宝くじの当選確率は、0 ではないなら、少なくとも 1 兆分の 1 以上あるはずだ」
視点 B（解析的な視点）：
一方、関数の性質を詳しく調べると、その値は「非常に小さくなる」ことがわかります。
- 例：「実は、この宝くじの当選確率は、1 兆分の 1 よりも遥かに小さい、ほぼ 0 に近い値だ」

③ 決定的な矛盾

「0 ではないなら大きいはず（A）」と「実はすごく小さい（B）」という、真逆の結論が出ます。
これは、**「最初に仮定した『答えは代数数である』という前提が間違っていた」**ことを意味します。
したがって、答えは「超越数」でなければなりません。

4. コンピュータ証明の難しさ：穴埋めと接着剤

人間の証明では、「ここは明らかだから省略」という部分があっても許されました。しかし、コンピュータ（Lean）は「明らか」を許しません。

穴埋め： 関数が特定の点で「消える」際、数学的には「穴」ができます。人間は「まあ、そこは埋められるよね」と済ませますが、コンピュータは「具体的にどう埋めるのか、式で示せ」と要求します。
接着剤： 著者たちは、この「穴」を埋めるために、関数を複数の部分に切り分け、それぞれの部分で厳密に定義し、最後にそれらを完璧に接着する作業を行いました。これは、**「壊れた橋を、一つ一つのボルトを計算しながら修理して、再び通行可能にする」**ような作業でした。

5. なぜこれが重要なのか？

数学の信頼性向上： 複雑な証明をコンピュータで検証することで、人間が見逃していたミスを防ぎ、数学の基礎をより強固にします。
未来への架け橋： この技術を使えば、もっと難しい問題（例えば、 $e + \pi$ が有理数かどうかといった未解決問題）や、暗号技術に関わる数論の問題も、将来的にコンピュータで検証できるようになる可能性があります。

まとめ

この論文は、**「100 年前の天才数学者が解いた『数字の正体』の謎を、現代の AI（コンピュータ）が『ゼロから再検証し、完璧な証明書として完成させた』」**という物語です。

それは、数学という古い城を、最新の技術を使って「耐震診断」し、さらに「完全な設計図」を書き直すような、壮大で緻密な作業でした。

論文「Gelfond-Schneider 定理の形式化」の技術的概要

Michail Karatarakis と Freek Wiedijk によるこの論文は、証明支援系 Lean 4 およびその標準ライブラリ Mathlib を用いて、数論における重要な未解決問題であったヒルベルトの第 7 問題（およびその解決である Gelfond-Schneider 定理）を完全に形式化したことを報告しています。

以下に、問題の背景、手法、主要な貢献、結果、および意義について詳細にまとめます。

1. 問題の背景と目的

Gelfond-Schneider 定理: 代数的数 $\alpha$ ( $\alpha \neq 0, 1$ ) と無理数である代数的数 $\beta$ に対して、 $\alpha^\beta$ は超越数であるという定理です。
歴史的意義: 1934 年に Gelfond と Schneider によって独立して証明され、超越数論の基礎を築きました。これにより、 $2^{\sqrt{2}}$ や $e^\pi$ （Gelfond 定数）などの具体的な数の超越性が確立されました。
形式化の課題: 既存の形式化プロジェクト（Coq, Isabelle/HOL, HOL Light など）では、 $e$ や $\pi$ の超越性証明や Liouville 数の超越性は扱われていましたが、Gelfond-Schneider 定理のような「補助関数（auxiliary function）」の構成や、代数的整数論と複素解析を深く結びつける高度な定理の形式化は行われていませんでした。
目的: Lean 4 環境下で、この定理の証明を完全に機械検証可能な形に再構築し、Mathlib への貢献を通じて超越数論の形式化基盤を強化すること。

2. 手法と技術的アプローチ

証明は、代数的な下限（数論的性質）と解析的な上限（関数の増大度）の矛盾を導くことで構成されます。形式化においては、古典的な紙面上の証明を厳密に Lean の型理論に適合させるための多くの技術的工夫がなされました。

A. 代数的数論の基盤構築

代数体のハウス（House）の定義:
- 代数的整数 $\alpha$ の「大きさ」を測る指標として、共役なすべての値の絶対値の最大値（ハウス）を定義しました。
- 従来の多項式の根の最大値に基づく定義（Finset.max'）では、共役の順序付けや線形関係の扱いが困難でした。
- 解決策: 標準的な埋め込み $K \to \prod_{\sigma: K \to \mathbb{C}} \mathbb{C}$ を用い、これを Banach 代数（ supremum ノルム付き）として扱う構造を採用しました。これにより、Mathlib のノルム空間 API を利用して、三角不等式や乗法性などの性質を自動的に導出できるようになりました。
Siegel の補題の一般化:
- 整数環 $\mathbb{Z}$ 上の Siegel の補題（未定方程式系における小さな整数解の存在）を、代数体の整数環 $\mathcal{O}_K$ へと一般化して形式化しました。
- 線形系を $\mathbb{Z}$ 上のより大きな系に変換（descent argument）し、 $\mathcal{O}_K$ 上の係数を持つ「小さな」非自明な解の存在を証明しました。これは、補助関数の係数を構成する上で不可欠です。

B. 補助関数の構成と解析的評価

補助関数 $R(z)$ の構成:
- 特定の点で高次の零点を持つ指数関数の線形結合 $R(z) = \sum \eta_i e^{\rho_i z}$ を定義します。
- Siegel の補題を用いて、係数 $\eta_i$ が代数的整数であり、かつそのハウスが十分に小さいことを保証しました。
特異点の扱いと全関数 $S(z)$ の構築:
- 証明の核心となる関数 $S(z)$ は、古典的には $R(z)$ を $(z-\ell_0)^r$ で割った形式で定義されますが、整数点 $1, \dots, m$ に極（pole）を持ちます。
- 技術的課題: Lean において、極を持つ関数を定義すると、定義域の制限や部分関数（partiality）の扱いが証明を複雑にします。
- 解決策: $S(z)$ $S (z)$ を「極を持つ有理関数」としてではなく、**全関数（total function）**として再構築しました。
  - 特異点 $l$ において、 $R(z)$ が $r$ 次でゼロになる性質を利用し、局所的な正則関数因子 $R'_U(z)$ を抽出します。
  - 特異点以外では通常の有理式を、特異点ではこの局所因子を用いた値を定義し、これらを「パッチング（gluing）」して、複素平面全体で正則な関数 $S(z)$ を構成しました。
  - これにより、Cauchy の積分公式を適用する際に、特異点を避けるための複雑なドメイン管理を不要にし、解析的な評価を厳密に行うことができました。

C. 矛盾の導出

代数的下限: $\rho = (\log \alpha)^{-r} R^{(r)}(\ell_0)$ が代数的整数の倍数であることを示し、そのノルムが 1 以上であるという下限（ $|N(\rho)| \ge 1$ ）を導きました。
解析的上限: Cauchy の積分公式を用いて、 $S(z)$ の増大度を評価し、 $\rho$ の絶対値が $r$ が大きくなるにつれて指数関数的に減少する上限を示しました。
矛盾: 十分大きな $r$ に対して、代数的下限と解析的上限が矛盾することを示し、 $\alpha^\beta$ が代数的数であるという仮定を否定しました。

3. 主要な貢献

初の完全形式化: Gelfond-Schneider 定理の完全な形式化は、定理証明系において世界初です。
Mathlib への貢献:
- 代数的数論における「ハウス（house）」の概念と、その代数的性質の形式化。
- 代数体上の Siegel の補題の一般化。
- 特異点を持つ関数を全関数として扱うための複素解析ライブラリの拡張（可除特異点の処理など）。
定数管理の明示化: 古典的な証明では $O(\cdot)$ 記法や一般的な定数で済まされることが多い部分を、 $c_1$ から $c_{15}$ まで具体的な定数として明示的に追跡・形式化しました。これにより、矛盾が生じるための具体的なパラメータ条件（ $q$ の大きさなど）を厳密に導出しています。

4. 結果

定理の証明: Lean 4 において、 $\alpha \neq 0, 1$ かつ $\beta$ が無理数である代数的数であれば、 $\alpha^\beta$ は超越数であることを証明しました。
具体例の検証: 形式化された枠組みを用いて、Gelfond-Schneider 定数 $\sqrt{2}^{\sqrt{2}}$ が超越数であることを具体的に導出しました。
コードの公開: 形式化されたコードは Mathlib のブランチに公開されており、コミュニティによる再利用や拡張が可能となっています。

5. 意義と将来展望

超越数論の形式化基盤の確立: この作業は、超越数論の形式化における重要なマイルストーンです。単なる孤立した定理の証明ではなく、補助関数構成や Siegel の補題といった一般的な手法をライブラリ化しました。
今後の拡張性:
- Baker の定理: 対数の線形形式に関する Baker の定理（Gelfond-Schneider の一般化）への拡張が自然な次のステップです。
- p-進 Gelfond-Schneider 定理: 複素解析の部分を p-進解析（Schnirelmann 積分）に置き換えることで、Mahler や Veldkamp の結果を形式化できます。
- 楕円曲線と Schanuel 予想: 指数関数の代わりに Weierstrass の $\wp$ 関数を用いることで、楕円曲線や Abel 多様体に関する超越性定理（Schneider-Lang 定理など）や、Schanuel 予想の形式的検証への道が開けます。
決定手続きへの応用: 明示的に導出された定数管理は、特定の超越数に対する線形独立性の自動検証や、決定手続きの実装への応用可能性を示唆しています。

総じて、この論文は、高度に抽象的な数論的証明を、型理論と計算機検証の厳密な枠組みの中でどのように実現するかを示す、実用的かつ理論的に深遠な成果です。