第1回：Lean 4 は有限要素法研究に何をもたらすか

Introduction

Lean 4 と有限要素法をつなぐための準備ノート
(8th June 2026 Update)

近年，AI4Math，形式推論，自動証明支援，Mathlib などの発展により，数学を「人間が読む証明」として書くだけでなく，「計算機が検証できる証明」として整理する流れが強くなっています．Lean 4 はその中心にある定理証明支援系の一つです．公式サイトでは，Lean は正しく保守可能で形式的に検証されたコードを可能にする，オープンソースのプログラミング言語かつ証明支援系として説明されています．

この連載では，Lean 4 を単なる流行語として扱うのではなく，有限要素法，異方性メッシュ，誤差評価，平衡化フラックス，DWR 型目的量評価といった数値解析の理論を，将来的にどのように検証可能な知識として整理できるか，という観点から眺めます．

1. Lean 4 は何をする道具か

Lean 4 は，プログラミング言語であると同時に，数学の定理や証明を形式的に記述するための証明支援系です．通常の数学論文では，「明らかに」「同様に」「標準的議論により」と書ける部分があります．しかし，Lean ではそのような省略は原則として通用しません．定義，仮定，補題，証明の各ステップを，計算機が確認できる形で記述する必要があります．

これは一見すると面倒です．実際，面倒です．鉛筆で一行の証明が，Lean では十行になることもあります．しかしその代わり，証明のどこに暗黙の仮定があるか，どの補題に依存しているか，どの定義が再利用可能かがはっきりします．これは，有限要素法のように仮定と定数依存性が複雑になりやすい分野では，大きな意味を持ちます．

2. なぜ FEM 研究者が Lean 4 を気にするのか

有限要素法の誤差解析では，多くの場合，次のような構造が現れます．

  • 連続問題の well-posedness
  • 有限要素空間の定義
  • 補間作用素や射影作用素の構成
  • 安定性評価
  • 補間誤差評価
  • Strang 型補題，inf-sup 条件，dual argument
  • a posteriori error estimator や certificate

これらは人間にとっては見慣れた流れですが，機械的に検証しようとすると，定義の粒度や仮定の置き方が非常に重要になります．特に，異方性メッシュでは，shape-regularity の代わりに，最大角条件，準正則条件，flatness parameter などの幾何量が登場します．このような条件を形式化するには，「要素とは何か」「辺長とは何か」「体積とは何か」「退化しないとは何か」を正確に定義しなければなりません．

つまり Lean 4 は，FEM をすぐに自動で証明してくれる魔法の杖ではありません．むしろ，FEM 理論をどの粒度で整理すべきかを突きつけてくる，かなり厳しい鏡です．鏡なので，見たくない定数依存性も映ります．そこがつらく，そして面白いところです．

3. まず形式化しやすい部分

いきなり「異方性メッシュ上の CR 要素の誤差評価」を Lean で完全形式化するのは，現実的には相当重いです．最初に狙うなら，次のような小さな部品がよいと思います．

  • 有限集合上の和と局所量の総和
  • ノルム・半ノルム・三角不等式
  • 単純な線形代数の補題
  • 一次元区間上の P1 補間
  • 参照要素から物理要素へのアフィン変換
  • 局所誤差評価から大域誤差評価への足し上げ

このあたりは，FEM の巨大な理論の中では小さな部品ですが，Lean で書くと「どの定義をどう再利用するか」という感覚が身につきます．最初から大聖堂を建てるより，まずレンガの形をそろえる，という感じです．

4. Lean 4 の最小例

Lean では，命題と証明を次のような形で書きます．これは純粋に論理の例です． 

example (P Q : Prop) (hP : P) (hPQ : P -> Q) : Q := by
  exact hPQ hP
意味は，「命題 \(P\)，\(Q\) があり，\(P\) が成り立ち，さらに \(P\) ならば \(Q\) が成り立つなら，\(Q\) が成り立つ」というだけです．数学的には当たり前ですが，Lean ではこの推論規則を明示します．

Mathlib を使えば，実数や代数構造，解析に関する豊富な定義や補題を利用できます．例えば，Mathlib を読み込んだ上で代数的な恒等式を tactic によって処理する，という方向に進めます． 
import Mathlib

example (a b c : ℝ) : a + b + c = a + (b + c) := by
  ring

ここで重要なのは，「Lean が勝手に数学を発見した」というより，既存のライブラリと tactic を使って，人間が与えた命題を検証しているという点です．AI4Math の文脈では，この「人間の構想」と「機械による検証」の役割分担が重要になります．

5. FEM への接続：証明を certificate として見る

私の研究で扱っている平衡化フラックスや hypercircle 型評価，DWR 型目的量評価は，数値解に対して「この範囲に真の解や目的量がある」と示す certificate を与える方向です．Lean 4 のような証明支援系は，この certificate の理論的な部分を，より検証可能な形で整理するための道具になり得ます．

もちろん，数値計算そのものをすべて Lean の中で実行する必要はありません．むしろ現実的には，FEniCSx や FreeFEM などで数値計算を行い，その背後にある数学的主張，例えば「この estimator が上界を与える」「この幾何条件の下でこの補間評価が成り立つ」といった部分を形式化する方が自然です．

この意味で，Lean 4 は FEM 実装の代替ではありません．FEM 理論の「証明の骨格」を整理するための道具です．FEniCSx が計算の実験室だとすれば，Lean は証明の実験室です．白衣は不要ですが，忍耐は必要です．

6. この連載でやりたいこと

この連載では，次の順に進めたいと考えています．

  1. Lean 4 は有限要素法研究に何をもたらすか
  2. Lean 4 の命題・証明・tactic を最小例で見る
  3. Mathlib で実数・ノルム・有限和を探す
  4. 三角不等式と局所誤差評価の形式化練習
  5. 参照区間上の P1 補間を Lean 的に眺める
  6. アフィン変換とスケーリングをどう定義するか
  7. FEM 誤差評価を形式化する前に必要な部品表
  8. AI4Math と certified FEM：人間・AI・証明支援系の役割分担

最終目標は，Lean 4 でいきなり大きな FEM 定理を証明することではありません．まずは，自分の研究で繰り返し現れる補題や構造を，形式化可能な粒度に分解することです．これは論文執筆にも有効です．証明が Lean に入るかどうか以前に，「どこが定義で，どこが補題で，どこが定数依存性か」が見えるようになるからです．

参考リンク

ページの先頭へ