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 でも使われている。