Lean 4 と Claude を用いた環論の定理の形式化
ジョン・D・クック氏が、AIアシスタントClaudeを使ってLean 4で環論の定理を形式化した実験を紹介。セミノルムに関するpqr定理の証明に失敗した経験を踏まえ、今回は特定の環定理の形式的証明に成功。AIと定理証明支援系の連携による数学の形式化の可能性と課題を示している。
背景メモ
- **Lean 4** はマイクロソフト研究所・カーネギーメロン大などが開発する「証明検証器」兼プログラミング言語。数学の定理をコンピュータが厳密にチェックできる形（形式証明）に書き下すために使われる。
- **Claude** は Anthropic 社の大規模言語モデル（LLM）。著者はこれに Lean 4 のコードを生成させ、定理の形式証明を試みている。
- 本記事で扱うのは環論（代数学の一分野）の基本的な定理。リング（環）とは、整数のような「足し算・掛け算」ができる代数構造のこと。
- 著者（John D. Cook）は応用数学者・ソフトウェア開発者で、機械学習や数値計算について広く発信している。
- 以前の実験では成功したが、セミノルムの「pqr 定理」の形式証明は失敗。今回はリングの定理で試したという文脈。AI による形式証明の自動化がどこまで可能か、という研究／興味の一環。