Lean

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

Lean については, Quanta の記事を読むのが良い。 多くの数学者が mathlib という library を作ることにかかわっている。

• Lean
• mathlib

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 予想はまだ証明されていない, ということである。