LeanCopilot: Lean 4 の証明自動化に LLM を組み込む C++ バックエンド
LLMs as Copilots for Theorem Proving in Lean
ひと目でわかる
- これは何？
- LeanCopilot は Lean の tactic として LLM 推論を呼び出せるようにするパッケージで、C++ 製の推論バックエンドと Hugging Face 配布の小型モデルを組み合わせる。導入は lakefile のリンカ設定から始まり、Lean のバージョン整合が最初の関門になる。
- 誰に向いている？
- Lean 4 で mathlib を使った証明を書いていて、tactic 候補の提示や premise の絞り込みをエディタ上で回したい人には向く。逆に Lean のバージョンを頻繁に切り替える開発や、CUDA なしの環境で大きめのモデルを動かしたい用途には向かない。
- 商用利用できる？
- できます。MIT は寛容なライセンスで、著作権表示とライセンス表示を残せば、使用・改変・販売が可能です。
- 今もメンテナンスされている？
- されています。最後のコミットは 1 日前です。
- 何の言語で書かれている？
- 主に C++ です（GitHub の言語統計による）。
回答はプロジェクトの GitHub データ（最終同期：2026年9月15日）と当サイトの分析に基づくもので、法的助言ではありません。
オープンソース詳細解説
LeanCopilot が埋める穴: tactic を書く手が止まる瞬間
Lean 4 で証明を書いていて詰まる場面は大きく 2 つある。次にどの tactic を打てばいいか分からない場面と、使えそうな補題が mathlib のどこにあるか分からない場面だ。LeanCopilot はこの両方に手を入れる。README によれば、suggest_tactics が tactic の候補を出し、select_premises が前提となりうる補題の一覧を返し、search_proof が LLM の生成した tactic と aesop を組み合わせて複数手の証明を探す。対象読者は Lean 4 と mathlib で日常的に証明を書いている人で、ターミナルとエディタを行き来せずに候補を得たい層だ。補助輪として使うのであって、証明を丸ごと生成させる道具として README は提示していない。
推論はどこで走るのか: C++ と CTranslate2 の位置づけ
LeanCopilot の主要言語は C++ で、lakefile に追加するリンカ引数がその構成をそのまま表している。README の例では moreLinkArgs に -L./.lake/packages/LeanCopilot/.lake/build/lib と -lctranslate2 の 2 つを指定する。つまり Lean 側のパッケージが、CTranslate2 をリンクした共有ライブラリを呼び出す形になっている。モデルは Hugging Face から取得し、lake exe LeanCopilot/download を実行すると ~/.cache/lean_copilot/ に展開される。配布されているのは ct2-leandojo-lean4-tacgen-byt5-small、ct2-leandojo-lean4-retriever-byt5-small、premise-embeddings-leandojo-lean4-retriever-byt5-small、ct2-byt5-small の 4 つで、いずれも byT5-small 系の小型モデルだ。ここは設計上の割り切りとして読める。巨大なモデルを同梱せず、CTranslate2 で量子化済みの小型モデルを既定にして、CPU でも動く範囲に収めている。GPU がある場合の CUDA と cuDNN は任意項目とされており、必須ではない。
導入は lakefile の 2 行から: moreLinkArgs と require の書き方
手順は README に明示されている。まず lakefile.lean の package ブロックに moreLinkArgs を追加する。lakefile.toml を使っている場合は moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"] を書く。次に require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION" を追加し、安定版なら v4.33.0 のようなタグ、最新の不安定版なら main を指定する。lakefile.toml では [[require]] に name、git、rev を並べる。ネイティブ Windows の場合は .lake/packages/LeanCopilot/.lake/build/lib を Path 環境変数に足す必要がある。その後 lake update LeanCopilot、lake exe LeanCopilot/download、lake build の順に実行する。README は Dockerfile と scripts/build.sh、scripts/build_example.sh も案内しており、ビルドで詰まったときの逃げ道が用意されている。
バージョン整合という最初の関門
README の警告は率直だ。プロジェクトの Lean バージョンは少なくとも lean4:v4.3.0-rc2 でなければならない。加えて、LEAN_COPILOT_VERSION は mathlib など他の依存と互換でなければならないと明記されている。これは Lean 界隈では珍しくない制約だが、LeanCopilot の場合はリンカ引数がパッケージ配置パスを直接指しているため、依存解決がずれるとリンク段階で失敗しやすい構造になっている。README 自身が「他の依存との互換性を確認せよ」と繰り返しているのは、ここが実際のつまずきどころだと示唆している。Lean のバージョンを上げるたびに LeanCopilot のタグも追従させる運用が前提になる。
select_premises の射程: 固定スナップショットという制約
select_premises は LeanDojo の retriever を使い、固定された Lean と mathlib4 のスナップショットから前提を選ぶ。README には mathlib4 のコミットハッシュ 3ce43c18f614b76e161f911b75a3e1ef641620ff が示されている。これは利便性と引き換えの制約だ。自分のプロジェクトがこのスナップショットより新しい mathlib の補題に依存している場合、retriever はそれを候補として返せない。逆に言えば、返ってくる候補はその時点の mathlib に実在することが保証される。premise 選択の精度を上げたいなら retriever 側を差し替える必要があり、README もそのために Model APIs と Bring Your Own Model の節を用意している。既定のまま使うなら、mathlib のバージョンを固定スナップショットに寄せるほうが噛み合わせは良くなる。
aesop との役割分担と、search_proof が万能でない理由
search_proof は LLM が生成した tactic を aesop に渡して多段の証明を探す。探索の本体は aesop 側にあり、LLM は候補を供給する役割だ。したがって aesop が届かない領域、たとえば探索空間が広すぎる定理や、aesop のルールセットに載っていない補題が鍵になる証明では、LLM の候補が良くても探索が終わらない可能性がある。README は search_proof の成功を保証していないし、探索の打ち切り条件についても記述がない。証明探索を自動化の主軸に据えるのではなく、suggest_tactics で手を動かしながら、行き詰まったときに search_proof を試す使い方が現実的だ。
代替手段との違い: エディタ拡張ではなく Lean の tactic であること
Lean の証明支援には、エディタや LSP の外側から補完を提供するアプローチもある。LeanCopilot はそれを取らず、import LeanCopilot した後に suggest_tactics、search_proof、select_premises を Lean の tactic として直接呼ぶ形にしている。違いは検証の扱いにある。tactic として呼ばれる以上、提案された内容は Lean の証明項としてそのまま検査にかかる。エディタ上の文字列補完であれば、採用した時点で別途コンパイルして確かめる必要がある。LeanCopilot の場合、候補が通らなければ Lean が弾く。この設計は、証明の正しさを Lean のカーネルに委ねたまま LLM を使えるという点で筋が通っている。一方で、Lean のコンパイルを経由しない用途、たとえば自然言語での数学的議論の補助や、Lean 以外の言語での証明支援にはそのままでは使えない。
導入判断と確認事項
ライセンスは MIT で、商用利用を含めて比較的扱いやすい条件だが、同梱モデルは Hugging Face 上の別配布物であり、それぞれのモデルカードの条件を別途確認する必要がある。ライセンスの解釈についてはここでは踏み込まない。保守コストの面では、LeanCopilot のリリースが Lean 本体と mathlib の更新に追随する形で出ている点を織り込んでおきたい。2026 年 6 月から 8 月にかけて v4.31.0、v4.32.0、v4.33.0 が短期間に並んでおり、安定版タグを使うなら追随の頻度はそれなりになる。導入前に確かめるべきは 3 つ。Lean のバージョンが lean4:v4.3.0-rc2 以上か。lakefile に moreLinkArgs を書ける構成か。そして LeanCopilot のタグと mathlib のバージョンが一致するか。この 3 点が揃わない限り、lake build は通らない。逆に揃えば、suggest_tactics を 1 回打って候補が出るかどうかが最初の動作確認になる。
編集部の結論
Lean 4 で mathlib を使った証明を書いていて、tactic 候補の提示や premise の絞り込みをエディタ上で回したい人には向く。逆に Lean のバージョンを頻繁に切り替える開発や、CUDA なしの環境で大きめのモデルを動かしたい用途には向かない。導入前に確認すべきは、自分のプロジェクトの Lean バージョンが lean4:v4.3.0-rc2 以上であること、lakefile に moreLinkArgs を書けること、そして mathlib 側のバージョンと LeanCopilot のタグが噛み合うことの 3 点。ここがずれると lake build の段階で止まる。
コミュニティノート