21時30分06秒>人類が現在持っている最も美しくて精密で強力な言葉である数学で>記述し直しているのが物理学という感じです。数学をより精密に記述しなおそうという試みもありますので紹介します。現在の数学の記述方法は自然言語にたよっています。その為かどうしても記述に論理的に不十分な要素が入り込んでしまうことがあります。多くの数学者がその検証に時間をかけるということをしているはずです。そこで論理的なものならコンピューターでチェックしてしまおうという考えがでてきました。コンピューターに理解できる数学言語を作ってそれで数学を記述することで論理的に記述できているかコンピューターにチェックさせるのです。以下がその言語の一つMizarの説明です。http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar4/ja_wframe/index.html成果としては以下のものが紹介されています。JORDAN曲線定理の完全証明が完成!http://e-learn.mine.nu/mizar/jordancurve.htmコメントをどうぞ※メールアドレスとURLの入力は必須ではありません。入力されたメールアドレスは記事に反映されず、ブログの管理者のみが参照できます。※なお、送られたコメントはブログの管理者が確認するまで公開されません。※投稿には管理者が設定した質問に答える必要があります。)に転載したものから。---科学雑誌「ニュートン」2009年5月号は、時間論特集です。)に転載したものから。)に転載したものから。ブライアン・グリーンの最新刊。)に転載したものから。---日経サイエンス別冊の時間モノが出てます。30このブログについて本業はプログラマでありながら、文章がICT業界を超えて大人気の中村正三郎のブログ。ICT関連の話題、セキュリティの話題からマスコミ、科学、お笑い、ちょっとHなネタまで硬軟織り交ぜ話題沸騰。詳しいプロフィールは、http://www.asahi-net.or.jp/~ki4s-nkmr/profile.htmlをどうぞ。さんは、情報省のスパイ\(^O^)/府中、分倍河原のラーメン、麺屋もろ。いまの限定は「新作担々麺」。アイデア商品:着るお一人様用こたつ、あったか脚入れヒーター、歩けるシュラフ、寝袋。BCヒューズボックス府中の航空自衛隊に宇宙軍(宇宙作戦隊(仮称))、でわかる情報省支配。