• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Formalization of geometric topology towards 4-dimensional Poincare conjecture

Research Project

Project/Area Number 15K13433
Research Category

Grant-in-Aid for Challenging Exploratory Research

Allocation TypeMulti-year Fund
Research Field Geometry
Research InstitutionChiba 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)
  • 2017 Annual Research Report   Final Research Report ( PDF )
  • 2016 Research-status Report
  • 2015 Research-status Report
  • Research Products

    (6 results)

All 2016 2015 Other

All Journal Article (1 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 1 results) Presentation (3 results) (of which Int'l Joint Research: 1 results,  Invited: 2 results) Remarks (2 results)

  • [Journal Article] Formalization of Bing's shrinking method in geometric topology2016

    • Author(s)
      Ken'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto
    • Journal Title

      Lecture Notes in Artificial Intelligence

      Volume: 9791 Pages: 18-21

    • DOI

      10.1007/978-3-319-42547-4_2

    • ISBN
      9783319425467, 9783319425474
    • Related Report
      2016 Research-status Report
    • Peer Reviewed / Int'l Joint Research
  • [Presentation] Formalization of Bing's shrinking method in geometric topology2016

    • Author(s)
      Ken'ichi Kuga
    • Organizer
      Conference on Intelligent Computer Mathematics (CICM2016)
    • Place of Presentation
      Bialystok, Poland
    • Year and Date
      2016-07-25
    • Related Report
      2016 Research-status Report
    • Int'l Joint Research
  • [Presentation] Wild Topology and Formalization2015

    • Author(s)
      久我 健一
    • Organizer
      Workshop on Formalization on Applied Mathematical Systems
    • Place of Presentation
      University of Hawaii at Manoa
    • Year and Date
      2015-09-25
    • Related Report
      2015 Research-status Report
    • Invited
  • [Presentation] 証明支援系を用いたトポロジーの形式化について2015

    • Author(s)
      久我 健一
    • Organizer
      トポロジーシンポジウム
    • Place of Presentation
      名古屋工業大学 ( 愛知県名古屋市 )
    • Year and Date
      2015-08-06
    • Related Report
      2015 Research-status Report
    • Invited
  • [Remarks] PICoq(Python Interface for Coq)

    • URL

      https://bitbucket.org/kenkuga/picoq

    • Related Report
      2017 Annual Research Report
  • [Remarks] BingShrinkingCriterion

    • URL

      https://github.com/CuMathInfo/Topology

    • Related Report
      2015 Research-status Report

URL: 

Published: 2015-04-16   Modified: 2019-03-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi