| 研究課題/領域番号 |
15K13433
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
幾何学
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
久我 健一 千葉大学, 大学院理学研究院, 教授 (30186374)
|
|---|
| 研究協力者 |
萩原 学 千葉大学, 大学院理学研究院, 准教授
山本 光晴 千葉大学, 大学院理学研究院, 教授
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| 研究課題ステータス |
完了 (2017年度)
|
| 配分額 *注記 |
3,770千円 (直接経費: 2,900千円、間接経費: 870千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2016年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2015年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
|
|---|
| キーワード | 幾何的トポロジー / ビング収縮法 / 形式化 / Coq/SSReflect / 数学の形式化 / 証明支援系 / 深層強化学習 / formalization / geometric topology / shrinking method / coq / ssreflect / ビング収縮定理 / COQ / SSReflect |
|---|
| 研究成果の概要 |
我々は幾何的トポロジーにおいて位相同型写像を作る基本的な手法を提供するビング収縮定理を証明支援系Coq/SSReflectを用いて形式化した。この定理は直感的には異なるように見える空間の間に位相同型写像を与える時に用いられる。この定理の重要な応用例の一つはフリードマンによる４次元ポアンカレ予想の解決であり、そこでは、キャッソンハンドルと標準的ハンドルの間の位相同型写像が構成される。我々は、この定理を形式化するために、まだ多くの形式化を必要とするが、本質的な困難は形式化に必要な膨大な時間だけであると考えている。我々は形式化の負担軽減の目的で、Coqへの簡単なpythonインターフェースも作った。
|
