著者

久我 健一 萩原 学 山本 光晴

出版者

千葉大学

雑誌

挑戦的萌芽研究

巻号頁・発行日

2015-04-01

---

我々は幾何的トポロジーにおいて位相同型写像を作る基本的な手法を提供するビング収縮定理を証明支援系Coq/SSReflectを用いて形式化した。この定理は直感的には異なるように見える空間の間に位相同型写像を与える時に用いられる。この定理の重要な応用例の一つはフリードマンによる4次元ポアンカレ予想の解決であり、そこでは、キャッソンハンドルと標準的ハンドルの間の位相同型写像が構成される。我々は、この定理を形式化するために、まだ多くの形式化を必要とするが、本質的な困難は形式化に必要な膨大な時間だけであると考えている。我々は形式化の負担軽減の目的で、Coqへの簡単なpythonインターフェースも作った。