こんにちは｜こんばんは。カエルのアイコンで活動しております @kyamaz 
1です。
はじめに
プログラミング言語 Lean とは
Lean はMicrosoft Researchを中心に開発されている定理証明支援系と純粋関数型プログラミング言語の2つの側面を持つプログラミング言語です。Lean（特に最新のLean 4）は、次のような特徴が挙げられます。
-
依存型理論（Dependent Type Theory）に基づく設計
Leanの最も強力な特徴は、型が値に依存できる「依存型」を採用していることです。これにより、プログラムの型定義の中に、そのプログラムが満たすべき数学的・論理的な仕様（性質）を記述できます。 -
定理証明支援系としての機能
Leanは、数学的な証明を計算機上で記述し、その妥当性を検査するツールです。ユーザーが構築した証明の論理的飛躍や誤りを厳密に検証し、定理が正しいことを保証します。 -
純粋関数型プログラミング言語
高機能な型システムを搭載し、記述したコードをコンパイルして、高速に動作する実行可能なバイナリを生成できます。 -
メタプログラミングと柔軟性
Lean 4では、言語自体を拡張する強力なマクロシステムが備わっています。これにより言語の構文を自分好みに変更したり、ドメイン固有言語（DSL）を構築したりできる高いメタプログラミングも可能です。
そして Lean の真価は数学ライブラリ Mathlib にあります。コミュニティ主導で 2018 年に開発が始まり、現在は 100 万行を超える形式化済み定理を擁している 世界最大の機械検証済み数学コーパス です。線形代数から代数幾何、解析、数論、圏論まで、現代数学のかなりの範囲が「機械が検算済み」の状態で利用できるようになっています。
近年の動きとしては、2023年にテレンス・タオらが 多項式 Freiman–Ruzsa 予想の Gowers–Green–Manners–Tao 証明を Lean に書き起こしました。テレンス・タオといえばフィールズ賞受賞者であり、素数の列の中に任意の長さの等差数列が存在する『グリーン・タオの定理』の証明で有名な天才といわれる現代数学者のひとりです。
また、2026年3月31日にZEN大学の数学研究センター（ZMC）より発表された「LANAプロジェクト」では、『abc予想』を証明したとして知られる京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論のLean形式化による検証が一つの目的となっているというニュースが最近では注目されています。
このように、現役の研究者が自分の最新定理を Lean で書く時代になってきているとして、Lean は注目されてきています。
本稿では、Lean 4 + Mathlib を使って、Wikipedia に載っているある数学的事実を検証してみようと思います。
なお、本稿はコンピュータが数式を検算する様子を眺めていただくことを目的としており、本稿の読者は Lean の前提知識は必要としません。
Wikipedia の Quintic function の「可解な5次方程式（Solvable quintics）」の項には次のような数学的な事実が書かれています。
ブリング・ジェラード形式の五次方程式 $x^5 - x - r =0$ は $r \in {\pm 15,\ \pm 22440,\ \pm 2759640}$（および $r = 0$）のときに限り $\mathbb{Z}$ 上で 2 次式と 3 次式の積に分解され、累乗根(冪根)で解ける．
$r = 0$ は自明なので省くと、この命題が何故 $\pm 15, \pm 22440, \pm 2759640$ の３組なのかは、詳細が Wikipedia には書かれていません。そこで本稿では、この主張を Lean 4 + Mathlib で検証してみようという試みです。
理論的な準備
ところで、ここにでてくる３つの数には、出典 Elia–Filipponi (1998) 2 をたどると豊かな背景があることを伺い知れます。 Lean 4 + Mathlib で検証する前に、やはり机上で理論的な考察が必要となりますので、準備しておきましょう。
5 次式 $x^5 - x - r $ が $\mathbb{Q}$ 上で既約な場合、ガロア理論により累乗根(冪根)で解けるかどうかは Dummit の判別式 3 によって決まります。Elia–Filipponi の Theorem 2 はこれを使って次を示しています。
定理 (Elia–Filipponi 1998). $r \in \mathbb{Z}$ について $x^5 - x - r$ が $\mathbb{Q}$ 上既約なら、その根は累乗根(冪根)で表示できない。
つまり閉形式の根を得るには $x^5 - x - r$ が可約でなければならないということです。そして$\mathbb{Q}$ 上で可約のときは $\mathbb{Z}$ 上でも可約（ガウスの補題）から、結局問題は「$x^5 - x - r$ が $\mathbb{Z}$ 上で可約となる $r$」を分類することに帰着しています。
そこで5次式のモニックな分解を考えると、その分解は$r=0$のときの自明となり、その場合を除くと次の形しかありません。
$x^5 - x - r = $ {モニックな2次式} $\times$ {モニックな3次式}
そして、Rabinowitz (1988) 4 によるとこの形式にできる $r$ は次のようにフィボナッチ数で表されることが示されています。
$$r^2 \in {F_{2j-1}^2 F_{2j}^2 F_{2j+2},\ \ F_{2j}^2 F_{2j+1}^2 F_{2j-2}}$$
ここで効いているのがフィボナッチ数の性質を示す次の Cohn の定理 5です。
- Cohn の定理
- 偶数インデックスのフィボナッチ数で平方になるのは $F_0 = 0,\ F_2 = 1,\ F_{12} = 144$ のみである．
この定理から上式が成立する条件で代入すると非ゼロな $r$ が
$$
\begin{equation}\begin{aligned}
r = & \pm F_4 F_5 \sqrt{F_2} = \pm 15,\\ & \pm F_9 F_{10}\sqrt{F_{12}} = \pm 22440,\\ & \pm F_{14} F_{15}\sqrt{F_{12}} = \pm 2759640
\end{aligned}\end{equation}
$$
の 6 つに限られることがわかります。
Lean 4 + Mathlib で形式化
それでは、上記の理論的な内容を Lean4 で形式化してみましょう。本稿では Lean4 や Mathlib についての詳細は知っている必要はありませんが、ここで出てくる tactic（戦術）は次の 4 つだけです。これらの役割だけは押さえておいてください。
| tactic（戦術） | 役割 |
|---|---|
ring |
可換環の恒等式を展開・整理して同値性を確認 |
nlinarith |
平方完成を含む(非)線形不等式を解く |
interval_cases x |
範囲が有限の整数 $x$ をすべて試す |
decide |
計算で決定可能な命題をコンピュータに任せる |
これだけ覚えておけば以降のコードは「何をやらせているか」が読めます。形式化は次の３ステップで見ていきましょう。
-
ステップA
6 つの $r$ で確かに 2 次 $\times$ 3 次 に分解できる -
ステップB
その分解で整数根は生じない -
ステップC
モニックな多項式 2 次 $\times$ 3 次に分解できる $r$ は$r=0$を含む 7 つに限る
ただし、Cohn の定理は Mathlib に含まれていませんが、ここでは Cohn の定理の証明まで示すことはしません。そこは証明なしに axiom として置くこととします。 axiom は本来「公理」とされ、無証明で真とされるものです。このディレクティブを用いて Cohn の定理は無証明で真として受け入れます。（後述しますが、Cohn の定理に関連した２つの事実を認めます。）
ステップA： 6 つの分解を書き下す
モニックな多項式 2 次 $\times$ 3 次の係数比較から、$a, b$ を 2 次因子のパラメータとしておくと
$$x^5 - x - r = (x^2 + ax + b)(x^3 - ax^2 + (a^2-b)x + (-a^3 + 2ab))$$
であり、この恒等式が成立する条件は
$$a^4 - 3 a^2 b + b^2 = 1,\qquad r = a b (a^2 - 2b). \tag{$\ast$}$$
このディオファントス方程式 $(\ast)$ の整数解は $(a, b) = (0, \pm 1),\ (\pm 1, 0),\ (\pm 1, 3),\ (\pm 12, 55),\ (\pm 12, 377)$ の10組です。最初の 4 つは $r = 0$、残りが各 $\pm 15, \pm 22440, \pm 2759640$ を与えます。つまり以下の各等式になります。
$$
\begin{equation}\begin{aligned}
x^5 - x \mp 15 &= (x^2 \mp x + 3)(x^3 \pm x^2 - 2x \mp 5) \\
x^5 - x \mp 22440 &= (x^2 \pm 12x + 55)(x^3 \mp 12x^2 + 89x \mp 408) \\
x^5 - x \mp 2759640 &= (x^2 \mp 12x + 377)(x^3 \pm 12x^2 - 233x \mp 7320)
\end{aligned}\end{equation}
$$
これを示すには、Lean では各等式が1行で終わります。
import Mathlib.Tactic.Ring
theorem factor_pos15 (x : ℤ) :
x ^ 5 - x - 15 = (x ^ 2 - x + 3) * (x ^ 3 + x ^ 2 - 2 * x - 5) := by
ring
theorem factor_pos22440 (x : ℤ) :
x ^ 5 - x - 22440
= (x ^ 2 + 12 * x + 55) * (x ^ 3 - 12 * x ^ 2 + 89 * x - 408) := by
ring
theorem factor_pos2759640 (x : ℤ) :
x ^ 5 - x - 2759640
= (x ^ 2 - 12 * x + 377) * (x ^ 3 + 12 * x ^ 2 - 233 * x - 7320) := by
ring
ring は両辺を展開して同じか確認するだけの tactic になりますが、桁の大きい整数係数の多項式を手で展開するのは気力が必要です。そんな「人が見つけてきた式を、機械に確かめさせる」にはこの形式化がもっとも素朴で強力な使い方となります。ここで負の $r$ も含めて 6 つまとめると次のような記述で示すことができます。
theorem reducible_of_special_r (x : ℤ) :
(x ^ 5 - x - 15 = (x^2 - x + 3) * (x^3 + x^2 - 2*x - 5))
∧ (x ^ 5 - x - (-15) = (x^2 + x + 3) * (x^3 - x^2 - 2*x + 5))
∧ (x ^ 5 - x - 22440 = (x^2 + 12*x + 55) * (x^3 - 12*x^2 + 89*x - 408))
∧ (x ^ 5 - x - (-22440) = (x^2 - 12*x + 55) * (x^3 + 12*x^2 + 89*x + 408))
∧ (x ^ 5 - x - 2759640 = (x^2 - 12*x + 377) * (x^3 + 12*x^2 - 233*x - 7320))
∧ (x ^ 5 - x - (-2759640) = (x^2 + 12*x + 377) * (x^3 - 12*x^2 - 233*x + 7320)) := by
refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> ring
ステップB：整数根がないことを確かめる
ステップAでは「分解できる」ことを示せましたが、この「分解できる」と「整数根がない」という事実は別の話です。対象としている 6 つの $r$ では、$x^5 - x - r$ は 整数根を持ちません。これは「2 次因子と 3 次因子のどちらも整数根を持たない」を確かめれば、$\mathbb{Z}$ が整域なので積が $0$ にはなりません。
2 次因子は実数全体で正
2 次因子は判別式 $D$ を用いれば全て $D \lt 0$ となり、最高次数の係数が1ですので、実数全体で正となります。
たとえば $x^2 - x + 3$ の判別式は $D = (-1)^2 - 4 * 3 = -11 \lt 0$ です。この命題を Lean で定式化するには、平方完成のヒントだけ渡せばよくて、次のように書きます。
import Mathlib.Tactic
lemma quad_pos_15 (x : ℤ) : 0 < x^2 - x + 3 := by
nlinarith [sq_nonneg (2 * x - 1)]
つまり「$(2x - 1)^2 \ge 0$ を使え」と教えると、nlinarith は
$$4(x^2 - x + 3) = (2x - 1)^2 + 11 \gt 0$$
を自分で組み立てて検証してくれます。残り 5 つの 2 次因子も同じパターンで示せます。
3 次因子は整数根を持たない
3 次因子は実根を 1 つ持つ（３次式のグラフを想像すると$x$軸と交わる点が必ず１つは存在します）ので、その実根を挟む 2 つの整数を境にして区間を分けて考えます。各3次式 $c_{r}(x)$ について、実根を挟む 2 つの整数 $m, m+1$ を取り、
$$
\begin{equation}\begin{aligned}
c_{r}(x) &= (x - m) * (常に正な 2 次式) + c_{r}(m) \quad & (c_{r}(m) < 0)\\
c_{r}(x) &= (x - (m+1)) * (常に正な 2 次式) + c_{r}(m+1) \quad & (c_{r}(m+1) > 0)
\end{aligned}\end{equation}
$$
という恒等式から、それぞれ $x \le m$ と $x \ge m+1$ で符号が確定します。$r=22440$の実根は $7 \lt \alpha \lt 8$ にひとつだけ、$r=2759640$の実根は $19 \lt \alpha \lt 20$ にひとつだけです。
$c_{15}(x) = x^3 + x^2 - 2x - 5$ は実根 $\alpha \in (1, 2)$ にあり、実根まわりで局所極大があるため全ての整数 $x$ について $c_{15}(x) \ne 0$ を示すには、
- $x \le -2$ で $c_{15}(x) \le -5 < 0$
- $x \ge 2$ で $c_{15}(x) \ge 3 > 0$
- $-1 \le x \le 1$ では $-1, 0, 1$ の 3 点を直接代入して調査
の 3 区間に分けて示します。
lemma cubic_no_root_15 (x : ℤ) : x^3 + x^2 - 2 * x - 5 ≠ 0 := by
intro h
rcases le_or_gt x (-2) with hle | hgt
· -- x ≤ -2: c(x) = (x+2) * (x²-x) - 5 ≤ -5
have hq : 0 ≤ x^2 - x := by nlinarith [sq_nonneg x]
have hb : (x + 2) * (x^2 - x) ≤ 0 :=
mul_nonpos_of_nonpos_of_nonneg (by linarith) hq
have id : x^3 + x^2 - 2 * x - 5 = (x + 2) * (x^2 - x) - 5 := by ring
linarith
rcases le_or_gt 2 x with hge | hlt2
· -- x ≥ 2: c(x) = (x-2) * (x²+3x+4) + 3 ≥ 3
have hq : 0 ≤ x^2 + 3 * x + 4 := by nlinarith [sq_nonneg (2 * x + 3)]
have hb : 0 ≤ (x - 2) * (x^2 + 3 * x + 4) := mul_nonneg (by linarith) hq
have id : x^3 + x^2 - 2 * x - 5 = (x - 2) * (x^2 + 3 * x + 4) + 3 := by ring
linarith
· -- -1 ≤ x ≤ 1 を直接列挙
have h1 : -1 ≤ x := by linarith
have h2 : x ≤ 1 := by linarith
interval_cases x <;> norm_num at h
Lean での証明では $c_{r}(x)$ を 「(正負が決まる1次式)$\times$(常に非負な2次式)$\pm$定数」に書き直すことで、区間ごとに掛け算の符号が確定し、定数項が残って不等号の向きが決まることを示します。明らかでない範囲（$r=15$の有限の中央にある範囲）は interval_cases の tactic が総当たりで潰してくれます。残り 5 つの 3 次因子も同じパターンで示せます。
2次因子と3次因子を合わせて証明すると、
theorem no_int_root_pos15 (x : ℤ) : x^5 - x - 15 ≠ 0 := by
intro h
rw [factor_pos15] at h
rcases mul_eq_zero.mp h with hq | hc
· linarith [quad_pos_15 x]
· exact cubic_no_root_15 x hc
となり、更に 6 個まとめた集合論的な記述は次のように示せます。
theorem no_int_root_of_special_r :
∀ r ∈ ({15, -15, 22440, -22440, 2759640, -2759640} : Set ℤ), ∀ x : ℤ,
x^5 - x - r ≠ 0 := by
intro r hr x
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hr
rcases hr with rfl | rfl | rfl | rfl | rfl | rfl
· exact no_int_root_pos15 x
· exact no_int_root_neg15 x
· exact no_int_root_pos22440 x
· exact no_int_root_neg22440 x
· exact no_int_root_pos2759640 x
· exact no_int_root_neg2759640 x
ステップC：それ以外の r ではモニックな 2 次 × 3 次に分解できない
さて次のステップが少し難しくなります。
$x^5 - x - r$ が $\mathbb{Z}$ 上で モニックな 2 次式 × モニックな 3 次式 に分解されるなら、$r \in {0, \pm 15, \pm 22440, \pm 2759640}$ に限る．
という逆向きの命題を示すことを目指します。順を追って見ていきましょう。
Step C-1：係数比較を Lean に書く
まず「すべての $x \in \mathbb{Z}$ で $x^5 - x - r = (x^2 + ax + b)(x^3 + cx^2 + dx + e)$ が成り立つ」ならば次のような係数 $a, b, c, d, e \in \mathbb{Z}$ の関係式が成立することをLeanで書きます。
$$\begin{equation}\begin{aligned}
& c = -a, \\
& d = a^2 - b, \\
& e = -a^3 + 2 a b, \\
& a^4 - 3 a^2 b + b^2 = 1, \\
& r = a b (a^2 - 2 b).
\end{aligned}\end{equation}$$
theorem factorization_implies_diophantine
(a b c d e r : ℤ)
(hfact : ∀ x : ℤ, x^5 - x - r = (x^2 + a*x + b) * (x^3 + c*x^2 + d*x + e)) :
c = -a ∧ d = a^2 - b ∧ e = -a^3 + 2*a*b ∧
a^4 - 3*a^2*b + b^2 = 1 ∧ r = a*b*(a^2 - 2*b) := by
-- 差の多項式: ∀ x, (a+c)x⁴ + (b+ac+d)x³ + (bc+ad+e)x² + (bd+ae+1)x + (be+r) = 0
have hP : ∀ x : ℤ,
(a + c) * x^4 + (b + a*c + d) * x^3 + (b*c + a*d + e) * x^2
+ (b*d + a*e + 1) * x + (b*e + r) = 0 := by
intro x; linear_combination -(hfact x)
-- x = 0, ±1, ±2 で評価して 5 本の連立 → Vandermonde で各係数 = 0
have eα : a + c = 0 := by linarith
have eβ : b + a*c + d = 0 := by linarith
...
-- 上から順に c, d, e, ディオファントス方程式, r を導出
have hc : c = -a := by linarith
have hd : d = a^2 - b := by ...
have he : e = -a^3 + 2*a*b := by ...
have hdio : a^4 - 3*a^2*b + b^2 = 1 := by ...
have hr : r = a*b*(a^2 - 2*b) := by ...
exact ⟨hc, hd, he, hdio, hr⟩
Step C-2：ディオファントス方程式をペル型に変換
最終的に残るのはディオファントス方程式
$$a^4 - 3 a^2 b + b^2 = 1.$$
これを $b$ の 2 次方程式と見ると、判別式が $5 a^4 + 4$ で、それが平方数でないと整数解 $b$ が出ない。実際、$b = (3a^2 \pm \sqrt{5a^4 + 4}) / 2$ なので、整数 $b$ の存在条件は $5 a^4 + 4$ が平方であることです。
これは代数的恒等式
$$(2 b - 3 a^2)^2 = 5 a^4 + 4 \tag{$\diamondsuit$}$$
として書けて、$u = a^2,\ v = 2b - 3a^2$ と置けば
$$v^2 - 5 u^2 = 4$$
というペル型方程式に帰着します。
これを Lean では、恒等式 $(\diamondsuit)$ を linear_combination で一発で示せます。
lemma diophantine_implies_pell (a b : ℤ) (h : a^4 - 3*a^2*b + b^2 = 1) :
(2*b - 3*a^2)^2 - 5 * (a^2)^2 = 4 := by
linear_combination 4 * h
これで「ディオファントス方程式の任意の解はペル型方程式の解」として形式化できました。
Step C-3：2 つの定理を引用する
ここから先で必要になるのは、次の2 つの既知の定理です。
(α) ペル＝フィボナッチ接続. 整数 $(u, v)$ が $v^2 - 5 u^2 = 4$ を満たし $u \ge 0$ なら、$u$ はフィボナッチ数．具体的には $u = F_{2k},\ v = L_{2k}$（$L_n$ はリュカ数，偶数インデックス）．
(β) Cohn の定理 (1964). 平方になるフィボナッチ数は $F_0 = 0,\ F_1 = 1,\ F_2 = 1,\ F_{12} = 144$ のみ．
(α) はリュカ・フィボナッチ恒等式：$L_n^2 - 5 F_n^2 = 4(-1)^n$ の偶数インデックス版で、これはカッシーニの公式（$F_{n-1}F_{n+1}-F_{n}^2=(-1)^{n}$）から導けます。(β) は Cohn の定理で本稿では既知を前提とした定理です。
この 2 つの定理を組み合わせると、
- $u = a^2$ は 平方 であり、(α) より $u = F_{2k}$ という形の 偶数インデックスのフィボナッチ数 でもある
- (β) より平方になるフィボナッチ数は $F_0, F_1, F_2, F_{12}$ のいずれか。(α) で偶数インデックスに絞られているため $F_1$ は除外され、$F_0, F_2, F_{12}$ のいずれか
- よって $a^2 = u \in {0, 1, 144}$のみ、すなわち $a \in {0, \pm 1, \pm 12}$
Mathlib には (α) も (β) も入っていないので、本稿ではこの 2 つの定理だけを axiom として置きます。
/-- Cohn (1964): 平方になるフィボナッチ数は F_0, F_1, F_2, F_12 のみ。 -/
axiom cohn_theorem :
∀ n : ℕ, IsSquare (Nat.fib n) → n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 12
/-- ペル＝フィボナッチ接続: v² - 5 u² = 4 の非負解 u はフィボナッチ数。 -/
axiom pell_5_4_implies_fib :
∀ u : ℤ, 0 ≤ u → (∃ v : ℤ, v^2 - 5 * u^2 = 4) →
∃ n : ℕ, u = (Nat.fib n : ℤ)
上の議論を Lean に書き起こすと次のようになります。
lemma a_sq_classification (a : ℤ)
(hpell_eq : ∃ v : ℤ, v^2 - 5 * (a^2)^2 = 4) :
a^2 = 0 ∨ a^2 = 1 ∨ a^2 = 144 := by
-- (α) で a² = F_n
obtain ⟨n, hn⟩ := pell_5_4_implies_fib (a^2) (sq_nonneg a) hpell_eq
-- a² が a.natAbs の 2 乗なので F_n も平方
have hsq : IsSquare (Nat.fib n) := ⟨a.natAbs, ...⟩
-- (β) を適用 → n ∈ {0, 1, 2, 12}
rcases cohn_theorem n hsq with hn0 | hn1 | hn2 | hn12
· left; rw [hn, hn0]; decide -- F_0 = 0
· right; left; rw [hn, hn1]; decide -- F_1 = 1
· right; left; rw [hn, hn2]; decide -- F_2 = 1
· right; right; rw [hn, hn12]; decide -- F_12 = 144
ここでdecide は「Lean に小さい計算を任せる」というtactic（戦術）になり、$F_{12} = 144$ などを Mathlib が定義から逐次計算してくれます。
次に、$a^2 \in {0, 1, 144} \Longrightarrow a \in {0, \pm 1, \pm 12}$ という $a$ の絞り込みを記述します。ここは純粋に整数の計算です。$a^2 = 1$ なら $(a-1)(a+1) = 0$、$a^2 = 144$ なら $(a-12)(a+12) = 0$ を linear_combination で出して、$\mathbb{Z}$ の整域性で場合分けとします。
lemma a_classification (a : ℤ) (h : ∃ v : ℤ, v^2 = 5 * a^4 + 4) :
a = 0 ∨ a = 1 ∨ a = -1 ∨ a = 12 ∨ a = -12 := by
...
rcases a_sq_classification a hpell_eq with ha2 | ha2 | ha2
· -- a² = 0 ⇒ a = 0
left; have : a * a = 0 := by linear_combination ha2
exact mul_self_eq_zero.mp this
· -- a² = 1 ⇒ a = ±1
have h1 : (a - 1) * (a + 1) = 0 := by linear_combination ha2
rcases mul_eq_zero.mp h1 with h | h
· right; left; linarith
· right; right; left; linarith
· -- a² = 144 ⇒ a = ±12
have h1 : (a - 12) * (a + 12) = 0 := by linear_combination ha2
rcases mul_eq_zero.mp h1 with h | h
· right; right; right; left; linarith
· right; right; right; right; linarith
Step C-4：各 a につき b を解く
$a$ が決まれば、ディオファントス方程式は $b$ の整数係数 2 次方程式
$$b^2 - 3 a^2 b + (a^4 - 1) = 0$$
を解けばよく、$b$ が決まります。各 $a$ で具体的に次のように因数分解できます。
| $a$ | $b$ の方程式 | 因数分解 | $b$ の解 |
|---|---|---|---|
| $0$ | $b^2 - 1 = 0$ | $(b-1)(b+1) = 0$ | $\pm 1$ |
| $\pm 1$ | $b^2 - 3b = 0$ | $b(b-3) = 0$ | $0,\ 3$ |
| $\pm 12$ | $b^2 - 432 b + 20735 = 0$ | $(b-55)(b-377) = 0$ | $55,\ 377$ |
このように、10 組の $(a, b)$ が得られます。
これを Lean で書くと、a_classification で得た 5 つの $a$ それぞれに対して、ディオファントス方程式から linear_combination で因数分解を得て、mul_eq_zero で $b$ を確定します。
-- a = 12 の場合の抜粋
· have h1 : (b - 55) * (b - 377) = 0 := by linear_combination hdio
rcases mul_eq_zero.mp h1 with h | h
· have hb : b = 55 := by linarith
subst hb; right; right; right; left; rw [hr]; ring -- r = 22440
· have hb : b = 377 := by linarith
subst hb; right; right; right; right; right; right; rw [hr]; ring -- r = -2759640
10 組の $(a, b)$ ペアと、対応する $r$ の値は$r = ab(a^2 - 2b)$ から計算して、下表のようにまとめられます。
| $(a, b)$ | $r$ | フィボナッチ数表記 |
|---|---|---|
| $(0, \pm 1)$ | $0$ | — |
| $(\pm 1, 0)$ | $0$ | — |
| $(1, 3)$ | $-15$ | $-F_4 F_5$ |
| $(-1, 3)$ | $+15$ | $+F_4 F_5$ |
| $(12, 55)$ | $+22440$ | $+F_9 F_{10}\sqrt{F_{12}}$ |
| $(-12, 55)$ | $-22440$ | $-F_9 F_{10}\sqrt{F_{12}}$ |
| $(12, 377)$ | $-2759640$ | $-F_{14} F_{15}\sqrt{F_{12}}$ |
| $(-12, 377)$ | $+2759640$ | $+F_{14} F_{15}\sqrt{F_{12}}$ |
ここまでの命題をつないで$r$を分類して示すと、次のように目的の主張が示せたことになります。
theorem r_classification (r : ℤ)
(hex : ∃ a b c d e : ℤ, ∀ x : ℤ,
x^5 - x - r = (x^2 + a*x + b) * (x^3 + c*x^2 + d*x + e)) :
r = 0 ∨ r = 15 ∨ r = -15 ∨ r = 22440 ∨ r = -22440
∨ r = 2759640 ∨ r = -2759640 := by
obtain ⟨a, b, c, d, e, hfact⟩ := hex
obtain ⟨_, _, _, hdio, hr⟩ :=
factorization_implies_diophantine a b c d e r hfact
-- 5 a⁴ + 4 が平方であることをディオファントス方程式から導出
have hpell : ∃ v : ℤ, v^2 = 5 * a^4 + 4 := by
refine ⟨2*b - 3*a^2, ?_⟩
linear_combination 4 * hdio
-- a の値を絞り込み
rcases a_classification a hpell with rfl | rfl | rfl | rfl | rfl
· ... -- a = 0: b = ±1 → r = 0
· ... -- a = 1: b ∈ {0, 3} → r ∈ {0, -15}
· ... -- a = -1: b ∈ {0, 3} → r ∈ {0, +15}
· ... -- a = 12: b ∈ {55, 377} → r ∈ {22440, -2759640}
· ... -- a = -12: b ∈ {55, 377} → r ∈ {-22440, +2759640}
各 ... の中身の概略は、linear_combination で因数分解 → mul_eq_zero で場合分け → subst; rw [hr]; ring で $r$ の値を確定します。
整数根のない場合に絞れば $r = 0$ は除外されており、最後に $r = 0$ なら $x = 0$ が整数根であることを除外して完成です。
theorem r_classification_no_integer_root (r : ℤ)
(hex : ∃ a b c d e : ℤ, ∀ x : ℤ,
x^5 - x - r = (x^2 + a*x + b) * (x^3 + c*x^2 + d*x + e))
(hno : ∀ x : ℤ, x^5 - x - r ≠ 0) :
r = 15 ∨ r = -15 ∨ r = 22440 ∨ r = -22440
∨ r = 2759640 ∨ r = -2759640 := by
rcases r_classification r hex with h0 | h | h | h | h | h | h
· -- r = 0 の場合 ── 整数根 x = 0 が存在するので hno と矛盾
exfalso
apply hno 0
rw [h0]; ring
all_goals tauto
おわりに
Elia–Filipponi の記法では、$x^k - x = n$ の正の実根を $x_n(k)$ と書きます。ここで得られた 3 つの数に対する正の実根は、それぞれ $x_{15}(5), x_{22440}(5), x_{2759640}(5)$ にあたります。この数の具体的な値は 3 次因子にカルダノ式を適用して、次のような閉形式が得られます。
$$\begin{equation}\begin{aligned}
x_{15}(5) &= -\dfrac{1}{3} + \sqrt[3]{\dfrac{115}{54} + \dfrac{\sqrt{1317}}{18}} + \sqrt[3]{\dfrac{115}{54} - \dfrac{\sqrt{1317}}{18}} \\
x_{22440}(5) &= 4 + \sqrt[3]{90 + \dfrac{\sqrt{862863}}{9}} - \sqrt[3]{-90 + \dfrac{\sqrt{862863}}{9}} \\
x_{2759640}(5) &= -4 + \sqrt[3]{3130 + \dfrac{\sqrt{726984777}}{9}} + \sqrt[3]{3130 - \dfrac{\sqrt{726984777}}{9}}
\end{aligned}\end{equation}$$
数値的には $x_{15}(5) \approx 1.7185$, $x_{22440}(5) \approx 7.4106$, $x_{2759640}(5) \approx 19.5135$ です。これらの数は $x^5=x+r$ の解の１つであり、このことから「5乗しても小数部分が同じ（つまり整数の差しかない）数」という不思議な性質をもっています。この特徴は、2次の場合では Filipponi (1992) 6 により黄金比 $\displaystyle \alpha = \frac{1+\sqrt{5}}{2}$ が「2乗しても小数部分が同じ数」であることが示されており、Elia–Filipponi はそれを 5 次に拡張した結果として紹介しています。
出典にある論文をなぞって Lean4 に形式化している様子をご覧頂きました。このように、Lean4 で数学することができます。いかがでしたでしょうか。
私 は未だうまく Lean4 を扱えるまでのスキルがありませんが、AI Coding の力を借りて本稿を書き上げられました。皆さまも生成AIの支援を借りて『Lean4 で数学する』ことを楽しんで頂けると嬉しいです。
ご一読いただきまして有り難うございます。
（●）（●） Happy Hacking!
/"" ＿＿""＼
本稿の環境
最後に、本稿を記載するために検証した環境を記しておきます。お手元の環境で検証する際に、動作が異なるときには参考になるかもしれません。検証環境
本稿のために使用した環境は以下となります。
- macOS: Tahoe 26.3.1 (chip: Apple M1)
- Lean
leanprover/lean4:v4.30.0-rc2 - Mathlib
master@85e6e1b4(2026-04-29)
参考文献等
-
@kyamaz は、オープンソース・コミュニティ『OpenQL』プロジェクト7を通じて、皆さんと共に量子情報・量子コンピューティングの分野で挑戦しております。引き続きどうぞ宜しくお願い致します。 ↩
-
M. Elia and P. Filipponi, Equations of the Bring–Jerrard Form, the Golden Section, and Square Fibonacci Numbers, Fibonacci Quarterly 36.3 (1998), 282–286. PDF ↩
-
D. S. Dummit, Solving Solvable Quintics, Math. Comp. 57.195 (1991), 387–401. ↩
-
S. Rabinowitz, The Factorization of $x^5 \pm x + n$, Math. Magazine 61.3 (1988), 191–193. ↩
-
J. H. E. Cohn, On Square Fibonacci Numbers, Proc. London Math. Soc. 39 (1964), 537–540. ↩
-
P. Filipponi, A Curious Property of the Golden Section, Int. J. Math. Educ. Sci. Technol. 23.5 (1992), 805–808. ↩
-
OpenQLプロジェクトは、量子コンピューターを扱うためのライブラリを開発するためのオープンソースプロジェクトです。量子情報、量子コンピューターに興味のある人たちが集うコミュニティを運営しております。詳しくはconnpassのサイトをご覧ください。 ↩