Formalization of geometric topology towards 4-dimensional Poincare conjecture
| 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
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2016: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | 幾何的トポロジー / ビング収縮法 / 形式化 / Coq/SSReflect / 数学の形式化 / 証明支援系 / 深層強化学習 / formalization / geometric topology / shrinking method / coq / ssreflect / ビング収縮定理 / 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.
|
Report
(4 results)
Research Products
(6 results)
