LeanでLLMを有効活用する (2026年9月版)

LeanでLLMを有効活用する（2026年9月版）。特別なことをせずエージェントに証明作業を任せることで、LLMを効果的に活用できる。過去にはLLMに書かせた証明が使えないと考えていたが、lake buildをエージェントに実行させ、エラーとして出力される未解決ゴールを基に証明を修正していくイテレーションで活用可能。

• LLMはAI定​​理証明支援系Leanの学習環境として強力で、OpenAIなどの企業が強化学習に活用し、その結果がモデルに焼き込まれた可能性がある。
• OpenAIがNavier–Stokes方程式の証明をLeanで生成するなど、LLMはLeanによる形式証明の自動生成能力を飛躍的に向上させた。
• 以前はLLMはタブ補完程度だったが、現在はエージェントがlake buildを実行し、エラー出力を基に自律的に証明を生成・修正できるようになった。
• LANAプロジェクトによるabc予想のLean形式化や、朝日新聞がLeanに言及するなど、定理証明支援系が一般の注目を集めるようになった。