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

数学の証明を formalize して, 証明を支援するシステムがいくつか開発されている。

2014年頃までの試みについては, Harrison と Urban と Wiedijk の [HUW14] にまとめられている。

私が最初に目にしたのは, Coq というものだった。

• 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

Proof assistant は, 他にも, 色々開発されているようである。 例えば, 次のようなものがある。

• Agda
• Isabelle
• Walnut [Mou]

これらは全て dependent type theory に基いたものであるが, どうして dependent type theory なのか, という誰しも思う疑問が, MathOverflow で質問されている。 Andrej Bauer による詳しい回答がある。

圏論, 特に高次の圏に関する proof assistant は, string diagram やその高次元版を用いたものが開発されている。

• Quantomatic
• homotopy.io

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

ただ, Harrison と Urban と Wiedijk の [HUW14] によると, 初期は証明支援システムではなく定理の自動証明の研究が主流だったようであるが。

このように, 数学の証明やその補助として computer program を用いることについて, Granville による Bulletin of A.M.S. の記事 [Gra24] がある。 その中で, computer system にも必ず error があることが指摘されているが, 確かにその通りである。また, 単に正しいことを確認するだけの証明ではなく, 理解の助けになる証明が欲しいとも言っている。

References

[GCS]

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

[Gra24]

Andrew Granville. “Proof in the time of machines”. In: Bull. Amer. Math. Soc. (N.S.) 61.2 (2024), pp. 317–329. arXiv: 2305.02329. url: https://doi.org/10.1090/bull/1826.

[HUW14]

John Harrison, Josef Urban, and Freek Wiedijk. “History of interactive theorem proving”. In: Computational logic. Vol. 9. Handb. Hist. Log. Elsevier/North-Holland, Amsterdam, 2014, pp. 135–214. url: https://doi.org/10.1016/B978-0-444-51624-4.50004-6.

[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.

[Mou]

Hamoon Mousavi. Automatic Theorem Proving in Walnut. arXiv: 1603.06017.

[The]

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