LeanでLLMを有効活用する (2025年7月版)

要約: 証明以外を書くのに使うと面倒な仕事が減ってよいです。

Cursor

年額プランで契約しちゃったので使ってます

• 自動補完で出てくる証明はほとんど使い物にならない。大目に見積もって精々2割くらいが採用可能か
  • Proof Summitで聞いた話でも肌感覚はこれくらいっぽい
  • Leanのフォーマッタが無いので手でインデントを整えているのだが、tabで自動補完が暴発するのが不愉快
• 個々の証明が書けないので、例えばリポジトリ全体に対して自律的に証明を書かせるみたいなユースケースも無理だろう
  • 普通の関数定義を書いてもらうのはできた気がする
• リファクタリングはたいへん便利
  • 関数のパラメータを消すとか変数のリネームとか証明を微妙に書き直すとかのパターン化された編集をファイル全体に/ファイルを跨いで適用するといったケース
  • 最初の数回を手で編集すると次の編集をサジェストしてくれるのが概ね正しくてよい
    • IntelliJのような優れたIDEが提供してくれるリファクタリングツールのほうが精度も速度もよい。一方でLeanのようにIDE体験への投資が追いついてないケースや文脈に沿っていい感じに変更してほしいときなどはLLMでやったほうが楽。破壊的イノベーションだね
• VSCodeのコマンドを実行できない。特にRestart Lean Serverを実行できないのが痛くて、リポジトリ全体で証明を修正したいときに別ファイルの変更をインポートできなくて詰む
• 既存のコードを読むのは得意。証明以外なら書けるので、最近はrebarベンチマークのドキュメントを読んでベンチマーク用のコマンドを書いたりTOMLにエントリを追加してもらったりした

Devin

$40課金

• エディタを開かずにSlackでお願いするとタスクをやってくれるのがすごい
• 証明は書けない
• 細々としたタスクをやってもらうのがよい
  • ドキュメンテーションを書いてもらう (例)
  • リファクタリング
    • 証明は自分で書く (例)。まあこれは証明の直し方が非自明なのである程度仕方ない…
• 一番役に立ったのはGood First Issueを作ってもらったこと (例)
  • 作ってから1ヶ月で3人コントリビュートしてくれる人が出てきてくれた
  • 正規表現エンジンという題材に興味がある人はそこそこいるのだと思う。そこにGood First Issueを作ったことで一歩踏み出せるようになったのかな
  • 一人でやってたらGood First Issueを作る気には絶対ならなかったので、めちゃくちゃコスパがいい
  • 提案する実装方針とかは細々とした点が普通に間違ってるのでそこは気をつけたほうがよいです

Claude Code・Gemini CLI

まだ使ってない。どうですか？

Lean系MCPツール

• あるらしいです
  • lean-lsp-mcp: https://github.com/oOo0oOo/lean-lsp-mcp
  • LeanTool: https://github.com/GasStationManager/LeanTool
• 定理証明支援系はInfoViewに表示されてるProof Stateがたいへん重要なので、自律的に証明を書いてもらうにはMCP経由で読んでもらう必要があるんじゃないかと睨んでいる

自動証明モデル

• あるらしいです
  • DeepSeek Prover v2: https://github.com/deepseek-ai/DeepSeek-Prover-V2
    • 一番強いらしい
  • Kimina Prover: https://github.com/MoonshotAI/Kimina-Prover-Preview
    • 次に強いらしい
• いい感じに実用できるようになってほしい