数学とコンピュータの悩ましい（？）関係
http://wired.jp/2013/04/09/computers-and-math/
定理が成り立つかどうかをコンピュータに判定させる事の是非が論じられているらしいですが、これって詰将棋の世界でも過去に似たケースがあったんでしょうかね。
私の感覚では「作った詰将棋が完全作かどうか」って判定はコンピュータ任せで良い様な気がしますが、これも詰将棋ルーチンの発展前（df-pnが出る前位？）では話が違ってくるでしょうし。
話は戻って数学の方。
単純に「定理が成り立つかの証明」を目的とするなら、その為の手段としてコンピュータを使うのは効率面で良い事でしょう。ただ、「定理の証明の過程で、汎用的に役立つ手法*1を構築する」事を目的とするなら、それはコンピュータには荷が重い気がします。
この辺は一言で「数学」と言っても色々分野があるらしいんで、部外者がどうこう言っても無意味でしょうか。
ただ、人工知能の研究をしていた一人としては、人間の知的活動の一部をコンピュータに肩代わりさせるのは人工知能の進歩の証ですし、そういう面では数学にコンピュータを利用するのは「アリ」なんじゃないかと思います。
