🔢 mathematics

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

この論文は、Lean 4 とその数学ライブラリ Mathlib を用いて、アドルフ・フルヴィッツの解析的アプローチに基づき、平面における古典的な等周不等式（ $L^2 \ge 4\pi A$ ）を形式的に検証したものである。

原著者： Miraj Samarakkody

公開日 2026-03-17

📖 1 分で読めます🧠 じっくり読む

原著者： Miraj Samarakkody

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

この論文は、**「数学の証明を、コンピュータに『絶対に間違っていない』と確認させる」**という壮大なプロジェクトについて書かれています。

タイトルにある「等周問題（Isoperimetric Problem）」とは、一言で言えば**「同じ長さの紐で囲める一番広い面積は、どんな形？」という問題です。答えはご存知の通り「円」**です。

しかし、この「円が一番広い」ということは、古代ギリシャの時代から直感的には分かっていたものの、それを**「絶対に間違いなく、論理的に証明する」**のは非常に難しかったのです。

この論文では、20 世紀の天才数学者アドルフ・フルヴィッツが考案した「フーリエ級数（波の足し合わせ）」を使ったエレガントな証明を、**「Lean 4（リーン・フォー）」**というコンピュータ用の証明アシスタントを使って、一歩一歩、コンピュータにチェックさせました。

以下に、専門用語を避けて、わかりやすい例え話で説明します。

1. なぜコンピュータで証明する必要があるの？

通常の数学の教科書にある証明は、人間が「まあ、ここはこうなるよね」という**「暗黙の了解」や「直感」**を頼りに進められることが多いです。
しかし、コンピュータは「直感」が分かりません。「なぜここがこうなるのか？」と、すべてのステップを厳密に説明しないと、証明を認めてくれません。

この論文の著者は、**「人間の直感に頼らず、すべての論理のつなぎ目をコンピュータにチェックさせた」**のです。これにより、その証明が「100% 間違っていない」という確実性が得られます。

2. 証明のストーリー：「波」を使って「形」を測る

フルヴィッツの証明は、幾何学（図形）の問題を、**「音楽の波（フーリエ級数）」**の問題に変換するところから始まります。

ステップ 1: 曲線を「波」に変える

閉じた曲線（輪っか）を、時間とともに変化する「波」の集まりとして考えます。

アナロジー: 複雑な形をした輪っかを、いくつかの「正弦波（サイン波）」や「余弦波（コサイン波）」を足し合わせて作られたものだと想像してください。
著者は、この「波の足し合わせ」が、元の輪っかを正しく再現していることをコンピュータに確認させました。

ステップ 2: パースヴァルの定理（エネルギーの保存）

ここが証明の肝です。

アナロジー: 「波の形そのものの大きさ（面積）」と、「その波を構成する成分（波の強さ）の合計」には、決まった関係があるという定理です。
簡単に言えば、「複雑な波全体のエネルギー」と「それを分解した小さな波のエネルギーの合計」は等しい、というルールです。
このルールを使って、輪っかが囲む「面積」と、輪っかの「長さ」の関係を数式で結びつけました。

ステップ 3: ウィルティングの不等式（「平均」の法則）

アナロジー: 「波が振れすぎないようにするルール」のようなものです。
このルールを使うと、「波の形（面積）」が、「波の傾き（長さ）」によって制限されていることがわかります。
ここでもう一つ、**「AM-GM 不等式（平均と幾何平均の関係）」**という、高校数学の有名なルールを使います。「2 つの数を足すより、その 2 つを掛け合わせた方が（ある条件下で）小さくなる」というような、シンプルな不等式です。

ステップ 4: 最終的な結論

これらのルールを全部組み合わせると、**「どんな形でも、面積は『長さの 2 乗』の 4π 分の 1 以下になる」**という式が導き出されます。

円の場合、この式は「等号（＝）」になります。
円以外の形だと、必ず「小于（＜）」になります。
つまり、**「円が最も効率的（面積が最大）」**であることが、論理的に証明されたのです。

3. 著者が直面した「地獄のような」難所

この証明は数学的には美しいですが、コンピュータにやらせるにはいくつかの「落とし穴」がありました。

「無限」と「積分」の入れ替え:
証明の中で、「無限に足し合わせる」と「積分する」の順序を入れ替える必要があります。人間なら「まあ、大丈夫だろう」と言えますが、コンピュータは「本当に大丈夫な条件（収束性）が満たされているか」を厳しくチェックします。著者はこの条件をすべてクリアさせるのに苦労しました。
「波の微分」:
波を微分（傾きを求める）する際、一つ一つの波を微分して足し合わせても、全体の微分と同じになるか？という問題です。これもコンピュータに厳密に確認させる必要がありました。
「座標」の扱い:
2 次元の平面（X 軸と Y 軸）を、コンピュータが理解しやすい「ベクトル（矢印）」の形に変換して扱う際、細かい定義の違いでエラーが起きやすかったそうです。

4. この研究の意義

この論文は、単に「円が一番広い」ということを再確認しただけではありません。
**「古典的な数学の証明を、現代のコンピュータ技術を使って、完全に再構築できる」**ことを示した点に大きな意義があります。

未来への架け橋: 将来、AI が数学の新しい定理を発見したり、複雑な物理現象をシミュレーションしたりする際、このように「厳密に証明された数学の基礎」が土台になります。
教育と理解: 「なぜ円が一番なのか」という問いに対し、直感だけでなく、コンピュータが追跡可能な「絶対的な論理」で答えることができました。

まとめ

この論文は、**「数学の古典的な名作を、最新の『デジタルの厳密さ』で再検証した」**という物語です。
著者は、コンピュータという「最も厳格な審査員」を前にして、フルヴィッツの証明が「完璧に正しい」ことを証明しきったのです。

まるで、「円が最強の形である」という古の知恵を、現代のデジタル技術で「100% 確実」というハンコを押したような作業だったと言えます。

論文「平面における古典的等周不等式の形式化」の技術的サマリー

Miraj Samarakkody によるこの論文は、数学証明支援系 Lean 4 とその数学ライブラリ Mathlib を用いて、平面における古典的な等周不等式（Isoperimetric Inequality）の証明を完全形式化（Formal Verification）したものです。特に、Adolf Hurwitz が 1902 年に発表したフーリエ級数を用いた解析的な証明アプローチに焦点を当てています。

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

1. 問題の定義

等周問題とは、「与えられた周長 $L$ を持つ平面図形の中で、最も面積 $A$ が大きいものは何か」という問いです。その答えは円であり、以下の不等式（等周不等式）として定式化されます。

$L^2 \ge 4\pi A$

等号が成立するのは、曲線 $C$ が円である場合に限られます。
この論文の目的は、この定理を「単純閉曲線（simple closed curve）」かつ「 $C^1$ 級（連続微分可能）」という条件下で、機械的に検証可能な形式証明として確立することです。

2. 手法と証明戦略

著者は、変分法（Calculus of Variations）ではなく、Adolf Hurwitz のフーリエ解析を用いた証明を採用しました。このアプローチは、幾何学的な問題を純粋な解析的な不等式の比較に帰着させる点で優れています。

証明は大きく 2 つのフェーズに分けて形式化されました。

フェーズ 1：フーリエ解析の基礎の確立

Hurwitz の証明に必要な解析的道具立てを Mathlib 上で構築しました。

三角関数の直交性: 区間 $[-\pi, \pi]$ における $\cos(nx), \sin(nx)$ の直交関係の形式化。
Parseval の定理: フーリエ級数の係数と関数の $L^2$ ノルムの関係を証明。
一様収束性: Weierstrass の M 判定法を用いたフーリエ部分和の一様収束の証明。
項別微分可能性: 級数の項別微分の正当性（一様収束性の条件付き）。
Wirtinger の不等式: 平均値が 0 である周期関数 $f$ に対して、 $\int f^2 \le \int (f')^2$ が成り立つことの証明（Parseval の定理を用いた導出）。

フェーズ 2：Hurwitz の証明の実行

単純閉 $C^1$ 曲線 $\gamma$ を弧長パラメータ $s \in [0, L]$ で記述し、これを $[0, 2\pi]$ 上に再パラメータ化して $f(\theta), g(\theta)$ とします。

面積公式: 靴紐公式（Shoelace formula）と Green の定理を用い、面積 $A$ を $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$ と表す。
部分積分: 周期性及び部分積分を用いて $A = \int f g' = -\int g f'$ を導き、 $A = \frac{1}{2} \int (f g' - g f') d\theta$ を得る。
AM-GM 不等式: $2fg' \le f^2 + (g')^2$ を適用し、 $A \le \frac{1}{2} \int (f^2 + (g')^2) d\theta$ を得る。
Wirtinger の不等式の適用: 重心を原点に移動させ $\int f = 0$ と仮定し、Wirtinger の不等式 $\int f^2 \le \int (f')^2$ を用いて、 $A \le \frac{1}{2} \int ((f')^2 + (g')^2) d\theta$ へと強化する。
弧長の制約: 弧長パラメータ化の条件 $\| \gamma' \| = 1$ より $(f')^2 + (g')^2 = (L/2\pi)^2$ が成り立つことを利用し、最終的に $A \le \frac{L^2}{4\pi}$ を導出する。

3. 主要な貢献と技術的課題

この形式化において直面した技術的課題と、それに対する設計判断が論文の重要な部分です。

無限和と積分の交換: 教科書ではしばしば省略される「和と積分の順序交換」を、Mathlib の Dominated Convergence Theorem（優収束定理）を用いて厳密に正当化しました。これには $L^1$ ノルムの和が有限であることの明示的な仮定が必要でした。
項別微分の正当化: フーリエ級数の項別微分を行う際、部分和の一様収束性と微分係数の一様収束性を両立させる必要があり、Lean の hasDerivAt_of_tendstoUniformly 定理を適用するための条件整備を行いました。
インデックスの不一致: フーリエ係数は通常 $n \ge 1$ で定義されますが、Mathlib の多くの定理は自然数 $n \in \mathbb{N}$ に対して定義されています。 $N^+$ （正の整数）と $\mathbb{N}$ の間のインデックス変換（シフト）を厳密に処理するロジックを実装しました。
ユークリッド空間と射影: 平面曲線を EuclideanSpace R (Fin 2) としてモデル化し、座標関数 $x(t), y(t)$ とベクトル値関数 $\gamma(t)$ の微分の関係を、PiLp 射影の微分可能性と合成関数の微分法則（チェーンルール）を用いて厳密に結びつけました。
積分の公式化: 靴紐公式や部分積分を、Lean の区間積分（IntervalIntegral）の文脈で再構成し、境界項が周期性により消滅することを証明しました。

4. 結果

論文は以下の主要な形式化成果を報告しています。

完全な形式証明: 等周不等式 $L^2 \ge 4\pi A$ の Hurwitz による証明全体が Lean 4 で検証可能となりました。
補助定理の確立: 三角関数の直交性、Parseval の定理、Wirtinger の不等式など、解析学における重要な定理が Mathlib 上で再実装・検証されました。
コードの公開: 完全な形式化コードは GitHub（https://github.com/mirajcs/IsoperimetricInequality）で公開されており、Mathlib の拡張として再利用可能です。

5. 意義と将来の展望

数学的厳密性の保証: 教科書の証明では「おおよそ」や「直感的」に扱われがちな技術的詳細（収束性の条件、微分の交換など）をすべて明示的に検証することで、証明の完全な信頼性を保証しました。
Mathlib の能力の示唆: 複雑な解析学（フーリエ解析、微分積分、測度論）の定理を、現代的な証明支援系でどのように構築・統合できるかのケーススタディとなりました。
将来の課題:
- 等号成立条件の証明: 現時点では不等式の導出に留まっており、「等号が成立するのは円の場合に限る」という部分の形式化は今後の課題です。
- 仮定の緩和: 現在の証明は $C^1$ 級曲線を前提としていますが、より一般の曲線（有界変動など）への拡張や、高次元への一般化（球面への拡張）が今後の研究目標として挙げられています。
- Parseval 関係の導出: 現在の主要定理では、フーリエ係数と関数の関係（Parseval 等式）を仮定として受け入れています。これを曲線の定義から直接導出する作業が次のステップです。

総じて、この論文は古典的な幾何学的不等式を、現代的な形式検証技術を用いて再構築した画期的な成果であり、数学の形式化における実力と可能性を示す重要な事例となっています。