⛳
LLMにLean4で証明を書かせてみる実験をした
Lean4で形式証明をLLMに書かせる実験をしてみた記録レポです。
実験環境について
まずエディタとして VSCodeを使用し、VSCodeのエージェントを使用することにします。
(Windowsマシンなら、ctrl + shift + I を押すと Copilot Chat の画面が開くので、そこでエージェントモードを選択します)
モデルは Calude Opus 4.5 を使用することにします。
そして、MCP として lean-lsp を使用します。lean-lsp のREADMEを詳しくは見てほしいですが、以下のような準備をします。
- Python のパッケージマネージャである uv のインストール
- ripgrep のインストール
-
mcp.jsonファイルの作成
実験に使用するファイル
以下のような Lean ファイルを用意しました。こいつの sorry 部分の証明をAIエージェントに埋めてもらうことにします。
variable {α : Type}
inductive List.IsChain (R : α → α → Prop) : List α → Prop
| nil : IsChain R []
| single (a : α) : IsChain R [a]
| cons_cons {a b : α} {l : List α} (hab : R a b) (hchain : IsChain R (b :: l)) :
IsChain R (a :: b :: l)
namespace List
variable {R : α → α → Prop}
theorem IsChain.reverse {l : List α} :
IsChain R l ↔ IsChain (fun a b => R b a) (l.reverse) := by
sorry
end List
プロンプト
まだあまり吟味していませんが、とりあえず暫定でこういうプロンプトを使いました。
AiTest.lean ファイル内の sorry で証明を埋めてある箇所について、証明を埋めてください。
ただし以下のことに気を付けてください。
* lake build を実行してエラーが出なくなるまで、作業を続けてください。
* 一つの定理の証明が長大にならないように、適切な補題を見つけて証明してください。
* simp タクティクと grind タクティクを上手に使って、証明が短く簡潔になるように努めてください。
結果
証明に成功しました。
生成してくれた証明がこちらです：
感想
- わりと難しい命題を与えたつもりだったんですけど、普通に解かれたのですごいなと思いました。
-
grindを使えと指示しているのに全然使わないのは困りますね。grindはまだ新しいタクティクなのでデータが少ないのかもしれないですね。解決策がわかりません。 - プロンプトで「証明が長大にならないようにね」と指示しないと、証明がだらだらと長くなっていました。適切な補題を見つける作業に誘導したほうが良さそうです。
Discussion