数学の証明のためのソフトウェア

数学の証明を formalize して, 証明を支援するシステムがいくつか開発されている。 私が最初に目にしたのは, Coq というものだった。

Kapulkin, Lumsdaine, Voevodsky [KL21], によると Four Color Theorem や Feit-Thompson Theorem が Coq により formalize されている。

Gross, Chlipala, Spivak [GCS] は, category theory を Coq に implement しようとしている。 Homotopy type theory の blog [The] によると colimit を扱うための library も開発されているらしい。

より新しいものとしては, Microsoft Research の Leonardo de Moura が開発した, Lean というものがある。 Lean については, Quanta の記事を読むのが良い。 多くの数学者が mathlib という library を作ることにかかわっている。

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

証明支援システムの次は, 当然定理の自動証明であるが, それについて Gowers が project を立ち上げている

References

[GCS]

Jason Gross, Adam Chlipala, and David I. Spivak. Experience Implementing a Performant Category-Theory Library in Coq. arXiv: 1401.7694.

[KL21]

Krzysztof Kapulkin and Peter LeFanu Lumsdaine. “The simplicial model of univalent foundations (after Voevodsky)”. In: J. Eur. Math. Soc. (JEMS) 23.6 (2021), pp. 2071–2126. arXiv: 1211.2851. url: https://doi.org/10.4171/JEMS/1050.

[The]

Homotopy Type Theory. Colimits in HoTT. url: https://homotopytypetheory.org/2016/01/08/colimits-in-hott/.