kmd710

Lean/Mathlib で量子力学のフーリエ変換：Schwartz 空間 $\mathcal{S}$ から $L^2$ へ（Parseval/Plancherel）

この記事は 証明支援系 Advent Calendar 2025 23日目の記事（2本目）です。
（一本目の記事「有限次元のスペクトル分解」は こちら ）

このGistページは、量子力学で使うフーリエ変換まわりの Parseval / Plancherel（特に「Schwartz 空間 $\mathcal{S}$ から $L^2$ への橋渡し」）を、Lean/Mathlib 上で動く形にまとめたものです。

参考（Wikipedia、リンク）：

量子力学では波動関数を $L^2$ 空間で扱い、運動量表示はフーリエ変換で与えられる。

kmd710

有限次元のスペクトル分解（Mathlib/Lean による表現）

概要

この記事は 証明支援系 Advent Calendar 2025 23日目の記事です。
（二本目の記事「量子力学のフーリエ変換：Schwartz 空間 $\mathcal{S}$ から $L^2$ へ（Parseval/Plancherel）」は こちら ）

本稿では、有限次元のスペクトル分解（自己共役 / エルミート行列の対角化） を、Mathlib の既存 API を使って Lean で表現できるかを検証します。 Lean や Mathlib の表記に馴染みのない方にも、見ただけでわかるような通常の数学表記（ 量子力学の数学的定式化 - スペクトル測度によるスペクトル分解 などで見られる標準的な表示形式）に近い形で記述することを目指します。

kmd710

Vericoding 実践メモ: 汎用 LLM と 汎用コーディングAIエージェントで Lean の形式証明を生成する

Read this in English (英語)

自然言語の曖昧な指示からコードを生成する vibe coding とは異なり、形式仕様に基づいて厳密に検証されたコードと証明を生成する vericoding が注目されています。本稿は、特定の数学の問題（IMO 1963 P5: 国際数学オリンピック1963年の第5問）について、最先端の汎用大規模言語モデル（LLM、GPT-5）と汎用コーディングAIエージェント（Cursor）を用いた、定理証明支援系 Lean による形式証明を生成した実践報告です。

---

背景: LLM とワークフローによる形式証明自動化の進展

ソフトウェアのバグは深刻な結果を引き起こしうるため、コードの正しさを数学的に証明する形式検証の重要性が増しています。しかし、その実施には多大な労力が必要でした。