めんどくさい証明を計算機に投げたい

大量の場合分けや長くて複雑な計算をやるような泥臭い証明が好きではない。そういう人は自分以外にもたくさんいるような気がする。別にはっきりした根拠はないけど，数学に対して「美しい」とか，それに近い形容をする人には，そういう傾向があるのではないかと思う。

ふと次のようなことを思った。仮に証明に出てくる場合分けやら計算やらが，単に手間がかかるだけで，機械的にできそうなものであったとしよう。その場合に，繁雑な証明を人手で行う代わりに計算機を使って済ませたとしたら，これはどうだろうか。好ましいと思われるだろうか。そうは思われないだろうか。

個人的には，証明を完成させるためにやるべき議論のパターンがはっきりわかっていて，あとは手を動かすだけだとしたら，計算機を使うのが正しい証明のありようであるような気がする。というのは，そういう状況では，実際の単調な証明をやって見せるのが人間だろうと計算機だろうと，たいした問題ではない気がするのだ。実際にそれで労力が削減されるということがどれほどあるかわからないけど，もし計算機による自動証明という形で証明が完成されれば，それはそれでいいような気がする。

じゃあ膨大な場合分けをしらみつぶしでやるだけでいいのか，もっと「美しく」やるべきではないのかという意見はあるだろうし，そう思う気持ちは理解できる。そうすべきだと感じることも多いかもしれない。ただ，今言いたかったことは，仮にしらみつぶしでやろうという方針が前提なら，人手でやるより計算機のほうが好ましいと思う，ということだ。なぜ，ということをきちんと説明するのは難しいけど，計算機に証明させられる部分を計算機に任せるのは，すべてを手でやるよりも賢いやり方であるように思う。

ぼくは大量の場合分けや長くて複雑な計算をやるような泥臭い証明をしたくないと思う。それは自分の手で証明をする場合にはいつでもそうなのだけど，もし計算機が代わりに証明してくれるなら，そして計算機に証明を任せようと考えたなら，計算機が吐き出すその証明がいくら泥臭いものであっても構わない(ことがある)と思う。別に証明は正しさの確認のためだけにやるのではないとは思っているけど，正しさを確認するためにする証明には(そういうのはめんどくさいだけでおもしろくなかったり，理解を深める助けにならなかったりすることも多いように思う)計算機が使えるなら使いたいと思うし，そういうときのための自動証明あるいは証明支援の技術が発達すればよいと思っている。