AI時代になぜLeanによる検証が必要なのか

生成AIは、コードも設計書も仕様も、証明らしき文章まで作れるようになった。便利になった一方で、AIの出力をそのまま正しいものとして扱うことには限界がある。AIは候補を高速に出せるが、その候補が要件を満たすか、境界条件を漏らしていないか、推論の途中で飛躍していないかは別問題だ。Lean 4は、AIに答えを作らせ、その答えを機械で検査する側を担うための言語であり、対話的定理証明支援系でもある。

AIの鬼の視点で言えば、Leanの価値は「真実を判定する魔法」ではなく、「信じてよい範囲を書面にさせる」ことにある。保証されるのは、Lean上に書いた仕様と前提のもとで性質が証明されていることだけだ。要件そのものの誤りや、仕様に書き忘れた業務ルールは、Leanが自動で補ってはくれない。だからこそ、AIが提案し、Leanが検査し、人が仕様の妥当性をレビューするという分担になる。AIに「それらしい答え」を量産させ、検査を通ったものだけを採用する。この順番を守るだけで、AIを過信する場面は大きく減る。

中小企業の実務で言えば、承認金額の上限や権限の判定など、間違えると被害が大きいルールから形式化の対象を1つ選ぶのが現実的だ。ルールを文章で書き、例と反例を作り、わざと壊す変更を1つ入れてLeanが止めるかを確かめる。全部を証明しようとしなくていい。守りたいルールを1つ、機械が読める形で書けたら、それが最初の成果である。AIに任せる範囲が広がるほど、この1本の価値は上がる。