Lean のコード生成に関しては、GitHub Copilot の補完AIやエージェントはほとんど役に立ちません（むしろ、邪魔しやがる）。コーディングAIの利用は現実的でないので諦めました。
とはいえ、Lean の複雑な言語仕様や巨大な Mathlib ライブラリを理解・把握できる自信はまったくありません。とうてい無理（「AIによるLeanコード生成の特殊性」参照）。
そこで、汎用LLM（のチャットボット）を手なずけて Lean コードを生成させようと試行錯誤しています。もともとは、Comet が「それ、わたし出来ます」と言ったので始めたことです。
「AI支援形式証明への道 報告-1 // Comet との経緯」
僕は、証明支援系を操るAI（LLM）としてその目的用に訓練された LLM が必要だろうと思っていました。ところが、（あくまで比喩的・擬人化した表現ですが）Comet が「それ、わたし出来ます」と言い出しました。Comet に自然言語で記述した定義・定理などを渡せば、Lean コードに翻訳して返せるとのことでした。
「AI支援形式証明への道 報告-2 off-the-shelf」より：
極端に比喩的・擬人化した例え話をするなら； 高級レストランを予約しないと食べられないと思っていたディナーを、「コンビニの食材だけ買ってきてもらえれば、わたし作ってあげるよ」と Comet が言ったようなものです。
しかし実際にやってみると、「おまえ、言うほど出来ねーじゃねーか」という場面は多いですね。汎用LLMではやはり限界があるのかも知れません。研究レベルでは、汎用LLMに対して Lean の知識・スキルを追加学習させた Lean 用LLMが存在するようです。将来的には、専門教育を受けたドメイン特化型LLM（Lean エキスパート）を使えるようになると期待してます。
現時点での汎用LLM（Comet）に「おまえ、なんで出来ないの？ なんで間違うの？」と問いただすと、言い訳ではない事情を答えます。
まず、Python や JavaScript/TypeScript などに比べて、Lean の学習データが圧倒的に少ない／足りない。「勉強する機会がなかったので出来ない」ということです。少ない学習データでも、Lean の専門教育として学習させれば効果が出るでしょうが、汎用LLMでは一般教養としてしか Lean を学習していません。
次に； 人間が Lean のコーディングをするとき、普通のプログラミング言語とは違うスタイルである点がAIにとってのネックになります。ソースコードを見ながらキーボードを叩く、というスタイルで Lean コードを書ける人はほぼいません（ごく少数の達人はいるかも知れません）。InfoView と呼ばれるモニター画面を見ています。
InfoView は、対話的 Lean 処理系の内部状態を観察できる画面で、デバッガやインスペクタに近いツールです。Lean コードを InfoView 無しで書くのは至難の技です。汎用LLMは InfoView にアクセスできないので、至難の技を強いられることになります。
今書いているコードや InfoView に見えている情報だけでは不十分です。それ以外の情報も必要です。例えば、インポートされているライブラリの機能・構造を知っている必要があります。すべての関連情報を把握しても、次にどう書くかは統計的パターンで類推できるとは限りません。コードの字面の統計的パターンだけで動く補完AIは、ほぼ間違えます。
Lean には、バージョン3とバージョン4があり、現時点ではバージョン4（Lean 4）が使われていますが、インターネット上の情報としては Lean 3 関連も多く残っています。そのせいで、AIは Lean 3 の構文（Lean 4 では廃止）を混ぜてしまうことがあります。Lean 4 では構文エラーになります。
「それ、わたし出来ます」「わたし作ってあげるよ」と Comet は言いましたが、「専門家ではない君にはちょっと荷が重かったかもな」という感じです。専門家LLMとは：
- 汎用LLMに、Lean の学習データを専門的に追加学習している。
- 運用時に、InfoView やライブラリの情報に完全にアクセスできる。
とはいえ、off-the-shelf（「AI支援形式証明への道 報告-2 off-the-shelf」参照）なツールとしては、当初の予想よりは、はるかに“使える”とも言えます。専門家LLMが使えるようになるまでは、専門家ではない汎用LLMと四苦八苦しながらの共同作業が続くでしょう。
- ハブ記事は「AI支援形式証明への道 報告-1」
