ハートレー・フォック近似

お、なんか楽しそうな予感

あらきけいすけさん経由 http://150.55.136.37/d200606.htm#628 で知ったのだけれども。

数学を表現するのに最適な媒体はコンピュータである 最上の日々
数学の限界が計算機の限界を規定する 404 Blog Not Found

まあ、色々いいたいことがある。
たとえば、不完全性定理激しく勘違いしてないかとか。

たとえば、僕は大学一年生の頃に暗号理論の研究室に遊びに行っていた。そこのポスドクの方が僕の相手をしてくれた(感謝してます)のだが、ある日彼は「今日はちょっと忙しいんだ。もうちょっとで証明できそうだから今日はあんまり相手してあげられない。」といって画面に向かっていた。何をしていたかというと、コンパイルした結果を見ながら TeX のソースをいじり、e のたくさんかかれた4*4くらいのでかい行列を変形していた。対角化なのかな。見ていて面白かった。

次の週に行ったら、なんかうれしそうに、「うん、できたんだよ〜。」って。
へえ。あれが論文になるんだ。

proof checker MIZAR
http://e-learn.mine.nu/mizar/jordancurve.htm

ああ、あと、 Coq の話が出てるんで、変化君あたり使い心地を教えてください(顔。

けれども、僕は HFA でエネルギー計算をしたのを印刷して大学にいく算段を立てる方が先決だ。
帰ってきたら寝ます。
起きたら書き直します。

おお、重要なこと忘れてた。
グレッグ・イーガンのディアスポラよろしく。

(追記:2006/07/10)
時が経つのは速い。書き直す気失せた。

ディアスポラに同じ疑問が出ていて、まあ、はい。

数学も実は帰納する学問で、論理的に展開してみて、それらを抽象概念に飛ばす。だからコンピュータを使って実験してみてから示す人は実は最近はいないわけではないようだ。

不完全性定理を勘違いしていないかといったのは、機械であろうが人であろうが記号操作をしているものは不完全性定理の呪縛から逃れられない、というところだ。現在、人が機械よりもよりよい数学者であるのは、数学の定理の「価値評価」というものが数学の外にあって、それは機械に教えられないからだ。