昨日の記事「AI支援形式証明への道 報告-1」で、AI支援〈AI-assisted〉の形式記述・形式証明について述べました。強調したい点は、紹介したやり方が off-the-shelf ベースであることです。"off-the-shelf" は、既製品、一般市販品といった意味です。特注品ではないモノです。イメージとしては、コンビニの商品棚（the shelf）から取り出して（off）買える品物が off-the-shelf なモノです。
もともと僕は、AI支援形式証明には特注品が必要だろうと想定していました。形式証明エキスパートとして訓練されたAI（LLM）や、特別に作られたMCPホスト／MCPサーバーなどです（「AI支援形式証明への道 報告-1 // 僕の想定」参照）。
しかし、Comet が「それ、わたし出来ます」と言い出したので（「AI支援形式証明への道 報告-1 // Comet との経緯」参照）、誰でも無料で手に入るソフトウェアツールを準備して試してみた、という次第です。
極端に比喩的・擬人化した例え話をするなら； 高級レストランを予約しないと食べられないと思っていたディナーを、「コンビニの食材だけ買ってきてもらえれば、わたし作ってあげるよ」と Comet が言ったようなものです。
コンビニの食材に相当するのが Lean と関連するソフトウェア一式です。具体的には：
- ツールチェインマネージャー elan
- ビルドツール兼パッケージマネージャー lake（elan によりインストール）
- 証明支援系 Lean 本体（elan によりインストール）
- コードエディタ VSCode
- VSCode拡張機能であるLean4拡張
いずれも off-the-shelf なソフトウェアです。そればかりか、すべて無料です。
AIも特注AIは不要で、現在ポピュラーなAIで十分です。Comet 曰く：
「自然言語を理解し、Lean 4 の基本構文・タクティクをそこそこ書ける LLM」であれば、そのまま他社・他モデルにも移植可能です。
特注品ではないので、運用上の不便さは残ります。Markdown文書をAIのチャット欄に貼り付ける、AIの出力を VSCode にコピペするといった単純作業は人間が担当します。幾分か「切ない」気分になってしまいます -- 「俺はコピペ係かよ」と。
しかし、コピペ作業は悪い面ばかりではありません。「AI ←→ 証明支援系」の通信・対話をすべて人間が手作業で仲介するので、ソフトウェアがやっていることがブラックボックス化することはありません。Lean のチェックが失敗して、エラーメッセージを参考にAIが修正するといった過程もすべて人間がモニターできます（つうか、モニターせざるを得ない）。
不便さ・面倒さは残ってはいるのですが、off-the-shelf なことは大きなメリットだと思います。キャッチフレーズは：
既製ツールだけでやるAI支援形式証明
「コンビニ食材だけで作る美味しいディナー」のノリです。
