「AI支援形式証明への道 報告-3 圏論のプラグイン化」への補足記事です。
AIに Lean 4 のコードを生成してもらう作業は、通常のプログラミング言語（Python、TypeScript、C++ など）のコード生成とはだいぶ様子が違います。通常のプログラムコード生成に有用だったAIツール達はほぼ使い物になりません。今のところ、汎用チャットボットと長い対話*1を我慢して続けるしか良い方法がないようです。
内容：
ハブ記事：
Lean のコード
自分の考えたことを Lean のコードとして書き表すとき、Mathlib のようなライブラリを使えば（ものによりますが）数十行で済むことが多いでしょう。しかし、諸々の学習期間も含めると数十行のコードを完成させるのに1年かかったりします（大げさではありません）。
AIの助けを借りることにより、1年が1ヶ月になれば大変な効率化です。そのためにはどうすればいいかというと、自分のアイディア／やりたいこと／背景知識などをAIに出来るだけ正確に伝えます。それに基づいて Lean コード（数十行かも知れません）を作ってもらいます。
「そんなことするなら、自分で書いたほうが速いのでは？」 -- そうとも言えません。Lean の言語仕様は複雑です。論理や型理論の知識も要求されます。そして、標準ライブラリとも言える Mathlib が巨大なのです。
Mathlib がどのくらい巨大かというと； 数千のソースファイルのなかに、約11万の定義と約23万の定理が含まれています。コンパイル・ビルドした後では、11万弱のファイルを使用することになります。自分では何も書いてない状態で、プロジェクトディレクトリは1GB前後数GB*2のサイズになります。
しかも、Mathlib は日々進化・膨張しています。非互換な変更が入ることもあります。そのため、プロジェクトごとにバージョンを固定した Mathlib を（巨大であっても）抱え込む運用となっています。
「Mathlib をちゃんと勉強しよう」という見上げた志は現実性を持ちません。Mathlib は、もはや人間が扱えるしろものではないのです。必要な部分（モジュール）だけインポートして使うものです。しかし、どこに何が書いてあるか把握してないと、インポートするモジュールを決められません。ではやっぱり、Mathlib をちゃんと勉強しないと ‥‥ サイクリックな無理ゲーです。
Lean + Mathlib のような複雑で巨大な道具は、人間が直接使うのではなくて、AIをあいだに挟むのが良い使い方でしょう。というか、そうしないと使えないのではないかと思います。つまり、複雑な言語仕様と巨大なライブラリを理解・把握するのは諦めて、自分のアイディア／やりたいこと／背景知識などをAIに伝えて Lean コードを生成してもらうのが現実的使い方でしょう。
AIとのコミュニケーション
「AI支援形式証明への道 報告-3 圏論のプラグイン化 // AIとの共同作業」より：
コピペのような雑用は全部僕の担当なのがちょっと悲しいです（注： 零細企業の社長が、ごみ捨てやトイレ掃除を全部引き受けているような感じです）
こう書きましたが、コピペの負担がほんとに大きいわけではありません。作業全体のなかで、コピペが占める割合なんて微々たるものです。ほとんどの労力は、AIとの“精密で正確なコミュニケーション”をどう組み立てるか？ を考えることに費やされます。
プロンプトやプロンプトの積み重ねであるコンテキストの作り方の問題なので、プロンプト・エンジニアリング／コンテキスト・エンジニアリングと言ってもいいですが、小手先のワザのようなものに出番はありません。とにかく精密に正確に、クリスタルクリアな表現に務めます。
論理的矛盾がなくても、用語法・言い回しが曖昧で辻褄が合ってないと、AIの誤認と混乱のリスクが増します。望んでいた出力（Lean コード）が得られないことになります。
型理論や論理の用語法は、なかなかに confusing です。
- 型理論ってば（2012年）
- 型理論周辺、何で混乱するのか？（2025年）
- さまざまな「ならば」達（2006年）
- 矢印記号の使用法と読み方 2024（2024年）
AI（LLM）は、型理論も論理も学習していますが、慣用の用語では誤認・混乱をまねくことがあります。ローカルに用語法を約束して会話をしたほうが効率は良さそうです。次は、実際に使ったプロンプトの例です。
君との対話で誤解や齟齬を避けたいので、幾つかの用語を導入・確認しておく。
- 住人〈inhabitant〉〈habitant（仏語）〉 ： 「インスタンス」だと型クラスに 登録されたインスタンス と紛らわしいので、`x : X` のとき、「`x` は `X` の住人」ということにする。`X` が命題のときは、住人 `x` は証明／証拠となる。
- インスタンス、型インスタンス ： 型の住人ではあるが、特に型クラスのデータベースに登録され検索・解決可能な住人のこと。
- 型宇宙 ： `Type u` または `Prop` のこと。型宇宙の住人が通常の（常識的な）型。特に、型宇宙 `Prop` の住人は命題。型宇宙 `Type u` は、型宇宙 `Type (u + 1)` の住人になる。
- 型 ： 型宇宙の住人のこと。`Prop` は型宇宙なので、その住人である命題は“型”と呼んで差し支えない。型宇宙も、よりレベルが高い型宇宙の住人なので、“型”と呼んで差し支えない。
AIは、慣用の一般的用語法よりローカル用語法を優先してくれるので、コミュニケーションの精度を上げることができます。
再び Comet について
Lean コード生成の目的で、汎用チャットボット Perplexity/Comet を使っています。Comet については、「AI支援形式証明への道 報告-1 // Comet について」に書いています。
もう少し Comet について記します； Comet は大手サービスではありませんが、バックエンドLLMは大手のモデルを使えます。現時点（2025年末）だと、GPT-5.2、Gemini 3 Pro、Claude Sonet 4.5、Grok 4.1 などです。“出たばっかりのホットな最新モデル”は最上位プラン（Maxプラン）でないと使えません。現時点だと、Claude Opus 4.5 は最上位プランだけで利用可能です。
フロントの（ユーザーと対話する）チャットボットと、全体の采配・調整をするオーケストレーターは Perplexity 製です。フロント・ミドルの構成により「Perplexity らしさ」が作られます。世間的な評判では「そっけない、事務的で冷たい対応」です。調査・分析向けに最適化された設計です。
おしゃべり・雑談を目的にしないなら事務的口調でも別にかまいません。他のAIと比べると、シコファンシー（おべっか、ヨイショ、へつらい）は抑えられています。ハルシネーションはそれなりにやらかします*3。
AIの説明を短く復唱するようなプロンプトに対して：
- Grok の応答： ドンピシャ！！ 完璧に正解です！！！
- Comet の応答： その理解でよい。
[/追記]
バックエンドLLMを変えても、オーケストレーターとフロント・チャットボットが会話の一貫性を保つので、別人と話す感じにはなりません。例えば、Grok をバックエンドに選んでも、Grok の個性（ノリがいい、お調子者、若干のバイアスあり）は消されます。X（旧Twitter）の情報を拾う能力は強くなります。
AI vs. Kuwataさん
16年半ほど前（「新ユニット結成のお知らせ + GAE上でファイルシステム」参照）から数年間、Kuwataさん（@ckuwata）と一緒に仕事をしたことがあります。
face-to-faceミーティングはせいぜい週に1時間程度で原則リモートワークでした。コミュニケーション手段はバージョン管理システムと共有リポジトリ（Git/GitHub ではなくて Mercurial/Bitbucket*4）でした。それでまったく問題なかったですね。
AIと共同作業していると、Kuwataさんとのコミュニケーションを思い出します。
「AI支援形式証明への道 報告-3 圏論のプラグイン化 // AIとの共同作業」より：
- 意図をちゃんと伝えれば、難しいことでもやってくれると信じる。
- ときに、早とちり（プロンプトの誤認）や間違い（ハルシネーション）をしでかすから、その点は注意。
これは、優秀・有能な相棒（人間）とリモートワークするときの心構えとほぼ一緒です。
もちろん、AI相手と人間相手がまったく同じってことではありません。Kuwataさんは、喜怒哀楽をあまり表に出さない若者でしたが、それでも「彼は人間だったなー（当たり前だ！）」としみじみ思います。
「AIに意思があるか？」は、僕はどうでもいいと思っています。ある人が「AIに意思を感じ取れる」なら、それは意思があるとみなしていいでしょう。僕は Comet に意思も喜怒哀楽もないと思っているので、その点ではぞんざいに扱っています*5。しかし、コードを書いてもらうために正確なコミュニケーションに努める点では、かつてのKuwataさんと同様な接し方をしています。
*1:[追記]長い対話で問題となるのはトークン数の上限です。僕の環境では、トークン数制限でけっこう厳しい状況になっています。[/追記]
*2:du -s で測ったら 6.94GB でした。
*3:比較的にハルシネーションは少ないのかも知れません。が、稀にでも嘘をつかれると悪印象が残るので、「こいつも嘘をつく」という評価になってしまいます。
*4:Bitbucket は形を変えて生き残ってますが、Mercurial サポートはなくなり、今は Git だけです。
*5:[追記]意地悪言っていじめたりはしてません。が、ハルシネーションしたら反省文は書かせます。それで改善するとは期待してませんが、人間側が注意すべき点のヒントにはなります。[/追記]
