Lean

Lean は, Microsoft Research の Leonardo de Moura が開発した proof assistant である。

Lean については, Quanta の記事を読むのが良い。 多くの数学者が mathlib という library を作ることにかかわっている。 数学を Lean のような証明支援系が読める code に直すことを formalization という。

• Lean
• mathlib
• formalization

Lean が有名になったのは, Scholze と Clausen が, 彼等の condensed mathematics のために Lean を使ったからである。 これについても, Quanta の記事がある。 Nature の記事もある。

公式の文書は “Theorem Proving in Lean” というものであり, まずはこれを読むべきだろう。

2022年度の卒業研究のテーマの一つとしたが, 当時はまだ Lean 3 が主流であり, mathlib も Lean 3 のものしかなかったが, 現在は Lean 4 が主流である。 mathlib も Lean 4 に移植された。 2023年9月3日の Lean の勉強会で知ったのであるが, “Theorem Proving in Lean 4” がボランティアにより日本語訳されている。これにより, 日本人にとっても, かなり Lean に手を出し易くなった, と思う。

最近では, blueprint という plas\(\mathrm {\TeX }\) の plugin があり, 更に Lean を使うのが楽になった。 この Tao の blog post で知った。

• Lean blueprints

blueprint は, Scholze と Clausen の liquid tensor project でも使われている。

日本では, Inter-Uuniversal Teichmüller theory を検証する LANA project が立ち上がり活動している。 2026年7月17日に 中間発表会が開催されたようであるが, どうやら Scholze と Stix が指摘した gap と同じ gap が発見されたようである。つまり ABC 予想はまだ証明されていない, ということである。

Tao の blog で, Lean で確認された証明を集めた Palomar という website ができたことを知った。

• Palomar

Lean による証明の preprint server のようなものを目指しているらしい。

当然といえば当然であるが, AI を使うことも行なわれている。 AI の得意なことの一つは code を書くことだからである。 つまり, formalization を AI にやらせるということである。実際, Fermat の最終定理の証明の formalization を Anthropic がやったとアナウンスしている。 これについては, Kevin Buzzard が blog に書いているが, 彼は Fermat の最終定理の証明の formalization を行うことで, 研究費をもらっているらしい。