Formalization of geometric topology towards 4-dimensional Poincare conjecture

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K13433
• Research Category: Grant-in-Aid for Challenging Exploratory Research
• Allocation Type: Multi-year Fund
• Research Field: Geometry
• Research Institution: Chiba University
• Principal Investigator: KUGA KENICHI 千葉大学, 大学院理学研究院, 教授 (30186374)
• Research Collaborator: HAGIWARA Manabu 千葉大学, 大学院理学研究院, 准教授 ; YAMAMOTO Mitsuharu 千葉大学, 大学院理学研究院, 教授
• Project Period (FY): 2015-04-01 – 2018-03-31
• Keywords: 幾何的トポロジー / ビング収縮法 / 形式化 / Coq/SSReflect

Outline of Final Research Achievements

We formalized Bing's shrinking theorem in geometric topology. This theorem provides a basic method to construct homeomorphisms between topological spaces in such circumstances where the topological spaces in question may look quite different. The most striking applications of this shrinking method include Freedman's solution of the 4-dimensional Poincare conjecture in 1981, where the two spaces in question are Casson's strange 2-handles and standard 2-handles. In our formalization, we used the proof assistant Coq/SSReflect. Although we still have much to go to formalize "Casson handles are standard 2-handles theorem", there seems to be no essential obstacle except for the need of a large amount of time. We made a simple python interface for Coq, which we hope may ease our work of formalization.

Free Research Field

トポロジー