『証明支援系を用いたトポロジーの形式化について』

久我 健一 , 証明支援系を用いたトポロジーの形式化について, 2015/08

1. どんなもの？

2. 先行研究と比べてどこがすごい？

3. 技術や手法のキモはどこ？

4. どうやって有効だと検証した？

5. 議論はある？

6. 次に読むべき論文は？

「形式化」とは、定理の証明の各ステップで、どの推論規則や公理が使われたかを例外なく全て記録すること

• 4-color theorem (Coq/Gonthier/2004)

• Jordan curve theorem (Mizar/Kornilovicz/2005, HOL light /Hales/2007)

• prime number theorem (Isabelle/Avigad et al/2007)

• Feit-Thompson theorem (Coq/Gonthier/2012)

• Kepler conjecture (HOL, /Hales/2014)