2023-03-25 のブログ記事「証明支援系がダメだった理由と、AIでブーストする理由」の最後の節を、ちょっと長いですが引用します。
以上に述べたような事情で、5年10年のレンジで見れば、証明ソフトウェアが普及することはないだろうと思っていました。一般の人（特別な資質と情熱の持ち主ではない！）が、教育目的や、ソフトウェア検証の目的で証明ソフトウェアを使うのは無理だ、と。
しかし、最近の幾つかの記事で指摘したように、にわかに事情が変わってきました。
自然言語の解釈と会話ができるAIの登場により、証明ソフトウェアの難点が解消される見込みが出てきました。この変化は、キャラクタUIからグラフィカルUIへの変化と少し似ています。ウィンドウシステムの登場により、ターミナル／コンソールのシェルに対して呪文のようなコマンドを打ち込んでは操作していたコンピュータが、直感的なマウス操作でもいじれるようになりました。
あるいは、プログラミングにおける高級言語の登場にも似てるかも知れません。機械語／アセンブラ言語は効率的ですが、人間向きとは言えません。機械語／アセンブラ言語しかなかったら、プログラミングは（一部の好き者以外には）難しくつらいものだったでしょう。
とは言いながら、コマンドシェルを好む人はいるし（僕も好きです）、GUIよりコマンドが効率的なときはあります。もちろんアセンブラ言語の使い手は今でも存在するし、リスペクトの対象です。自然言語に包まれた甘口の証明記述言語が普及しても、カチカチの形式言語の用途が消滅することはないでしょう。
「自然言語証明から形式証明を抽出できる（はず）」の最後に書いたように、証明の自動生成もけっこう期待できそう。証明自動生成においては「AIが間違えたり嘘を言ったりしないか？」という懸念は不要です。人間でもAIでも、証明ソフトウェアでチェックされるので、間違い・嘘はすぐに検出されます。
2年後くらいには、甘口の証明記述言語と良好な（できればピクトリアルな）ユーザーインターフェースが使えるようになっていると期待〈希望〉してます。そうなれば、「証明ソフトウェアは使いものにならない」という前言は撤回します。
この記事から「2年後」は今年（2025年）の3月ですから、現時点では2年8ヶ月たっています。「甘口の証明記述言語と良好な（できればピクトリアルな）ユーザーインターフェース」は出現したでしょうか？ してませんねー。
しかし、僕の希望的観測が“大幅に外れた”というわけでもないです。2年8ヶ月前に想定していた形とは少し違うのですが、自然言語からの形式証明はある程度は実現可能そうです。特別な道具ではなくて、今すぐ利用できるツール達の組み合わせで。
Perplexity Comet と質疑応答していて、以下のような暫定案に達しました。すぐ下は画面コピーで、その後にテキストも載せます。これは、Cometの応答ですが、AIにLeanの証明を書かせるプロンプトをAI（Comet）に出してもらったものです。この応答の前のプロンプトで僕がラフな案は出しているので、「AIに考えてもらった」のではなくて「AIに推敲と補足をしてもらった」です。
やりたいこと(目標)はその通りです。
- 日本語で書いた定義·定理·解答などについて、「Leanで形式化·証明できるかどうか」を通じて、その記述の論理的正当性を検証したい。
手順も基本そのままでOKですが、こう書き直すとより正確です。
- 私(人間)が、十分に明確な日本語(+必要なら数式)で、定義·定理·練習問題·模範解答を書く。
- あなた(AI=このLLM)が、その自然言語記述から Lean4 の定義·定理宣言·証明コードを生成し、あわせて「その Leanコードの意味」を自然言語で説明する。
- 私が、その Lean コードを VSCode+Lean 上でチェックしてみる(“実行”というより「型チェック+証明チェック」)。
- Lean が「証明済み(no errors)」になれば、その自然言語記述に対応する形式化は少なくともその論理体系の中で正しい、とみなしてOK。
- Lean 側でエラーが出たり、意味がズレていると感じた場合は、その Lean コードとエラー内容·違和感のポイントを、このチャットで共有し、私(人間)とあなた(AI)で
- 自然文の書き方を変えるか
- Leanでの形式化を修正するか
- もともとの主張(教材側)を直すかを検討する。
- このプロセスを、定理·補題·練習問題·模範解答について繰り返す。
ちょっとややこしいですが、AIが書き出した文面内の「私」は人間（より具体的には檜山）で、「あなた」がAI（より具体的にはComet）です。この文面自体はCometの出力で、コピーしてCometに（プロンプトとして）与える予定です。
段取りを一言でいうと； 汎用チャットAI（具体的にはComet）に自然言語プロンプトで Lean コードを生成してもらって、VSCode + Lean4拡張 でチェックする、というものです。
Cometが言うには（ひょっとすると身贔屓、自己アピールがあるかも知れませんが）、GitHub Copilot Chat を使うよりいいだろう、と。まー、GitHub Copilot Chat も試してみようとは思ってますが。
現在、Cometと細かい打ち合わせ(?)をしてます。うまくいくといいんだけど。
