計算機シミュレーションによる証明

http://www.yomiuri.co.jp/science/news/20070620i403.htm

原子を作る陽子や中性子に働く力の仕組みを、素粒子レベルで統一的に説明することに、筑波大大学院数理物質科学研究科の青木慎也教授らが、スーパーコンピューターを使った大規模な模擬計算で成功した。

http://www.asahi.com/science/update/0620/TKY200706200383.html

原子核を構成する陽子や中性子の間に働く「核力」と呼ばれる力を、スーパーコンピューターによる大規模計算で、素粒子（クォーク）のレベルから説明することに筑波大などのチームが成功した。４９年に日本人初のノーベル賞を受けた湯川秀樹博士の生誕１００年に、博士が提唱した中間子理論を、より根源的に証明したことになる。

朝日新聞の記事によると，Physical Review Lettersに載るそうです．電子版でしょうか？

数学者の方々は，不満を持ってこれらの記事を読んでいると思います（笑）
なんといっても，四色問題，いや，現在は四色定理．．．ちょっと岩波数学辞典で確認します．

4 色問題
［英］four color problem ［仏］probl`eme desquatre couleurs ［独］Vierfarbenproblem

（中略）
Appel とHaken（［2］，［3］）はKempe 鎖による可約性判定の大半が実は機械的にできることを見出し，Koch の協力を得て計算機チェックを行うことにより作業効率の大幅な改善を実現した．その結果彼らは1834 個の可約配置からなる不可避集合の構成に成功し，4 色問題を解決した．彼らの証明は検証しにくいものであったが，その後1997 年にRobertson，Sanders，Seymour とThomas［10］は633 個の可約配置からなる不可避集合を構成し，やはり計算機を使用しているもののはるかに検証しやすい証明を与えている．

やはり4色問題でした（証明されているのに）．
でもこの項を読むと，書いた方は計算機による証明に違和感を持っていることが分かります（「はるかに検証しやすい」と，さりげなく．．ちょっと四色問題とずれますが，この項の最後はこう終わっています：彼の証明は巧妙な帰納法による極めて短いものであり，計算機をまったく使わない．どなただろう？グラフ理論の人でしょうけど，あいにく岩波数学辞典第4版の執筆者は莫大であり，私にはどなただか予想がつきません．ただ，一時期，マスコミに良く出ていはった離散数学の専門家でヒゲの数学者，秋山仁さんのお名前はあります．秋山さんはグラフ理論の教科書を多数書いており，その中でアッペル・ハーケンの計算機を使った証明方法や，その基礎となったケンペの証明方法や放電法について詳しく解説されております．）．

これが物理学者だったら，計算機シミュレーションによる結果でも，数学者よりも遥かに容易く受け入れます．ブラックホール関係とか，「数値相対論」という学問分野があるくらいですから．

ちなみに私なら．．．最終的に，過程と結果が美しければ，計算機を使おうがどうがどっちでも良いです．