久我 健一
3/27(金)(11:15-12:15)
タイトル
On computer checking of the sphere to sphere theorem
アブストラクト
この発表では、Coq/SSReflectを用いたトポロジーの定理の形式化の話をした。
我々はBing収縮定理を形式化した
https://github.com/kenkuga/Bing_Shrinking_Criterion
その延長でフリードマンの球面-球面定理の形式化を行っているが、現段階では
まだ完成していない。
この発表では、このような形式化では、数学概念の一層の「抽象化」が必要であ
ることを、n次元球体を例に説明した。
また、位相空間の形式化の実際を簡単な実例で示した:
kuga20150320.html
kuga20150320.v