現代数学の系譜11 ガロア理論を読む22

現代数学の系譜11 ガロア理論を読む22at MATH

現代数学の系譜11 ガロア理論を読む22 - 暇つぶし2ch704:辜pスしていたと思いますが、何やら思わせぶりな題なので（おまけにアブストラクトとか内容紹介とか何も掲示が無かったので）ご尊顔を拝するだけのつもりで開始時間ギリギリに行ったら、もう教室はいっぱい。さすがフィールズ賞受賞者の講演です。後から入ってくる学生さん達に押されるように詰めていったら一番前の真ん中の席で聞く羽目になりました。(^^;; 面白かったので（いつもながら分かってませんが）紹介。詳しい内容は上のリンク先をご覧下さい。大雑把に言って数学の基礎を構成的/非構成的どちらも含み圏論（高次圏論）の公理化を含め Martin-Loef の型理論を含み homotopy 理論の世界を含むように作り、コンピューターで証明が出来る（少なくとも証明を検証できる）ようにしたい、という事。2005 年頃に Awodey と彼が独立に (Martin-Loef の) 型理論と homotopy 理論の類似に気がついたのが始まり。エピソード：ある事の証明に計算機が使えないかと思って数年前に検索してみた。まず Mizar というシステムが見つかった。これは普通の集合論を基礎にしていて、分かることは分かるが、例えば自然数の集合 {0,1,2,...} と非負整数の集合が等しいことを証明するのも大変（内部的な表現が大きく違う、などのため）。一方、もう一つ見つけたのが Coq で、これは計算機屋さんはよく使っているが、型理論に基礎を置き最初どうなっているのかさっぱり分からなかった。でも結局上記の如し。つづく

次ページ

続きを表示

1を表示