A Formalization of the Laplace Transform and Its Inversion in Lean 4

振り子の揺れ、ギターの弦の振動、あるいはワイヤーを伝わる信号のように、時間の経過とともに変化する物事の、乱雑で混沌とした動きが、瞬時にクリーンで静的な代数問題へと翻訳される世界を想像してみてください。これは、エンジニアや科学者によって一世紀以上にわたって使用されてきた数学的ツール、ラプラス変換の魔法です。これは、「時間」の言語（物事が動き、加速し、減速する世界）で書かれた物語を、「複素数」の言語（それと同じ動きが単純な乗算や除算になる世界）で書かれた物語へと変換する、ユニバーサルな翻訳機のようなものです。

なぜこれが重要なのでしょうか？ なぜなら、物事がどのように変化するかについての方程式を解くことは、引き絞られている結び目を解こうとするかのように、非常に困難なことが多いからです。しかし、その結び目を、単なる直線に見える別の言語へと翻訳することができれば、簡単に解いてから、答えを元の言語へと翻訳し直すことができます。この論文は、この翻訳機の「証明チェッカー」を構築することについて述べています。著者たちは単にルールを書き留めただけではありません。彼らはコンピュータプログラムであるLean 4を使用して、この翻訳機が、最もトリッキーな部分においてさえも、約束通りに正確に機能することを、ステップ・バイ・ステップで数学的に証明しました。彼らは、私たちが橋、回路、または制御システムを設計する際にこれらの強力なツールを使用する場合、その基礎となる数学が極めて堅牢であり、隠れたエラーがないことを確認したかったのです。

---

デジタル証明チェッカー

非常に厳格で、非常に文字通りに受け取る、数学は大好きだが推測を嫌うロボットの友人がいると想像してください。あなたはそのロボットに「これは、ぐにゃぐにゃした線を滑らかな曲線に変える公式だよ」と言いますが、ロボットは「本当に？ 線が激しく揺れすぎたらどうするんだ？ もし無限に続いていたら？」と聞き返してきます。この論文は、二人の研究者、ダニエルとアントワンが、そのロボットの友人に、ラプラス変換に関する必要な知識のすべてを教え込んだ成果です。

彼らは単に教科書を書いたのではありません。彼らはLean 4を用いた、コンピュータによって検証可能な完全なライブラリを構築しました。これは、コンピュータがエラーをチェックできる数学的証明を書くために特別に設計されたプログラミング言語です。彼らの目標は、ラプラス変換（時間を関数の形に変える手法）を取り上げ、基本的な定義から、答えを時間へと戻す複雑な「逆変換」のプロセスに至るまで、あらゆるルールが正しく機能することを証明することでした。

翻訳機と魔法の鏡

ラプラス変換は、魔法の鏡のようなものです。関数 $f(t)$（何かが時間とともにどのように起こるかを表すもの）を鏡に入れると、新しい関数 $(Lf)(s)$（同じことを「周波数」の世界で表したもの）が反射して戻ってきます。

• 順方向の旅： 論文では、もし関数が「行儀よく」振る舞う（無限大に向かって速すぎる勢いで爆発しない）ならば、この鏡は機能することを証明しています。彼らは、定数、時間の累乗、さらには正弦波のような単純なものをどのように翻訳するかというルールを証明しました。例えば、微分（変化率）が、単純に数値 $s$ の掛け算と初期値の引き算に変わることを示しました。これが、微分方程式を解くことをこれほど簡単にする「秘伝のソース」です。
• 逆方向の旅（逆変換）： 真の挑戦は、答えを取り戻すことです。反射を見たとき、元の物体が正確に何であったかをどうやって知るのでしょうか？ これはブロムウィッチ公式として知られる特定のメソッドです。

なぜ「簡単な道」を選ばなかったのか

通常、数学者は複素輪郭積分と呼ばれる手法を用いて逆変換の公式を証明します。地図上の図形の周りにループを描き、特別な定理（留数定理）を使って中の「宝物」を数える様子を想像してください。これは強力なツールですが、著者たちは、コンピュータのライブラリには、まだこれらの「地図を描く」ためのツールが十分に組み込まれていないことに気づきました。

そこで、彼らはより地面に近い、別のルートを取りました。複素平面にループを描く代わりに、問題を実世界の直線上の積分として扱いました。彼らは問題を、管理可能な小さな断片へと分解しました。

1. 切り捨て（Truncation）： 無限の線を、$-T$ から $T$ までの短い有限のセグメントであると仮定しました。
2. sinc関数： このセグメントを長くしていくにつれて、sinc 関数（波が次第に小さくなっていく形）を含む特定のパターンが現れました。
3. ディリクレ積分： 彼らは、このsinc波の下の面積に関する有名な、事前に証明された事実（ディリクレ積分）に依拠し、セグメントが無限に長くなるにつれて、結果が元の関数を完璧に再構成することを示しました。

このアプローチはセットアップこそ困難でしたが、実数の微積分に基づいていたため、コンピュータにとって検証しやすく、より安全なものでした。

振り子のテスト

彼らのシステムが実際に機能することを証明するために、彼らは単に抽象的な数学をチェックしたのではなく、古典的な物理学の問題である調和振動子を解きました。これは、揺れる振り子や跳ねるバネの背後にある数学です。

• 設定： 彼らは、静止状態から始まり、素早い押し出しを受けるバネを、$y''(t) + \omega^2 y(t) = 0$ という方程式で定義しました。
• 翻訳： 彼らはこの方程式を、コンピュータで検証されたラプラス翻訳機に入力しました。
• 結果： コンピュータは、この複雑な微分方程式を、単純な代数方程式 $(s^2 + \omega^2)Y(s) = \omega$ へと見事に変換しました。
• 解法： $Y(s)$ について解くと、$\frac{\omega}{s^2 + \omega^2}$ が得られました。
• 検証： コンピュータはその後、自身のライブラリをチェックし、この特定の結果がまさに $\sin(\omega t)$ のラプラス変換であることを確認しました。

これは大きな成功でした。これは、コンピュータが単に答えを計算しただけでなく、その答えが確かに正弦波であることを証明したことを意味します。これは人間が数世紀にわたって知っている事実ですが、人間のミスが入り込む余地のないレベルの確実性を伴っています。

ゲームの厳格なルール

この論文は、推測をやめて証明を始める際に、どれほど注意深くあるべきかについての教訓でもあります。著者たちは、教科書ではしばしば見過ごされがちな「落とし穴」をいくつか挙げています。

• 無限はトリッキーである： 積分が無限にいくと単純に仮定することはできません。証明では、関数の「裾」の部分が消滅するように、関数が十分に速く減衰しなければならないことを明示的に述べる必要がありました。
• エッジケース： 数学を進める際、ルールが変わる特定の点（例えば $t=0$ など）が存在します。コンピュータは、関数が正確にどこで定義され、連続しているかについて、彼らに精密さを強いました。
• 順序の入れ替え： 逆変換の証明において、2つの積分の順序を入れ替える必要がありました。日常的な数学では、単にこれを行うかもしれません。しかし、彼らの形式的な証明においては、結合された曲面の「面積」が有限であることを厳密に証明してからでないと、順序を入れ替えることが許されませんでした。

結論

この論文は、**形式検証（Formal Verification）**における金字塔です。これは新しい物理法則を発見したり、新しい種類の波を発明したりするものではありません。代わりに、すでに広く使用されているツールの周囲に、確信の要塞を築くものです。ラプラス変換とその逆変換をコンピュータがチェックできる言語に翻訳することで、著者たちは参照基準を作り上げました。

彼らは、関数が無限遠および開始時においてどのように振る舞うかという厳格なルールに従う限り、この「魔法の鏡」が機能することを証明しました。彼らは、答えへの道がショートカットではなく、注意深くステップ・バイ・ステップの論理に基づいていることを示しました。これらの数学的ツールに依存する次世代のソフトウェアを構築するすべての人にとって、この研究は、その基礎が単に強いだけでなく、壊れることのないものであることを保証しています。調和振動子の例は、最終的な承認の印として機能しています。コンピュータは人間と一致しており、初めてコンピュータがその証明に署名したのです。