別冊数理科学数学の未解決問題

図書室で借りて。

ええと、最後の複雑系と数学、っていうのは凄く電波なものを感じるのは私の頭が悪いから？引用の仕方とかがいかにも閉じた世界っぽい雰囲気が…ちとぐぐって…あー…

証明とプログラムの統一というのは面白かった。数学者は行為として証明し、発表する際に記述としての証明に変換する。計算機はそのどちらも解することはできず、形式的証明しか解することしかできない。形式的証明の形に落とせば、計算機に証明を確認させたり代行させたりすることができるかもですばらしい。例えば四色問題は計算機によって最初に証明された部分があるし、ゲーデルの不完全性定理は計算機によって検証されているらしい。ただ形式的証明は記述としての証明より大きく、そこに落とすのが面倒だとか、様々な理由で数学者は使ってくれない。ということで行為としての証明を支援するシステムを作ればいいとかなんとか。紙と鉛筆の変わりにそれを使えばいいとかなんとか。 maxima の凄いヤツみたいなのを作ってくれたらいいなあ。しかしそれは数学の未解決問題なのか？

リーマン予想とか Navier-Stokes とかは Clay の 100万ドル賞金でおなじみ。Shrodinger 方程式周りは難しいと聞いてたけどやはり難しいらしいとか。よくわかってないけど。

聞いたことはあった気がするけど、掛谷問題というのは面白いと思った。 http://www.hokudai.ac.jp/science/science/H16_08/sugaku/tachizaw.html くるくるくるりんというゲームがそれらしい。

あとは全然わからんものが多かった。世の中わかってないことが多くてすばらしい。それより自分がわかってないことが多すぎるのをなんとかしろ。