最上さんのところのネタ、とりあえず版
なんか、もう既に出遅れすぎのような気がしますが、数学者の端くれとしての感想を。もっとも、id:yoriyukiさんやid:bonotakeさん経由の萩谷先生のエッセイでもうかなり言われてしまっているのですが。
必要なのはむしろデータベース？
ずっと前に書いてある定義とか、どこに証明があるのだかわからない補題とか、standardだからいいよねとかしか書いてない議論とか、そういうので困った経験はもちろん私にもあります。ですので、そういう場面が少なくなるといいなとは思います。
でも、証明をmachine readableに近付けることでやるのは手間がかかりすぎるかと。そうではなく、十分使える検索機能を持つデータベースを作る方が早いし有効だと思います。それに加えて、読みながら気がついた点を他の人が補完できるようなwikiのような仕組みがあればなお良いかと。そういうページをとある集合論の概念に関して作ってみようかと思ったことがあるのですが、今のところは挫折中です。本業の方が優先ですので、やはり。
現在のような教科書とかsurvey paperを書くだけでも、新しい定理を証明する能力がある人たちに時間を大きく消費させてしまっているわけで、これ以上の負担を優秀な人たちに押し付けるよりは、それぞれのレベルの人が協力し合ってやった方が効率的かと思います*1。web2.0とか言ってもらえるかもしれないし。
数学の表現って
数学の論文が、定義、定理、証明が続くばかりだからといって、数学の表現がそれらだけで終わるというわけではありません。むしろ、イメージやそれを補強する例の方が重要かもしれません。少なくとも私は、自分の証明がmachine readableに書き直されたとしても、それが私のやったことを表現し尽くしているなんて思えません。
そして、「どこで定義されているのかわからないけれどもその分野では常識になっている記法」とかっていうのは、その分野に特有のイメージを伝えるために長年かかって作り上げられてきたものであって、それらを書き下してしまったら伝えたかったイメージがばらばらになってしまいかねないです。
最上さんはそのあたりは「良いシステム」ならば上手く回避できるという意見だと思うのですが、私はかなり懐疑的です。
というわけで、私にとって数学を表現するのに最適なメディアは黒板とチョークとガチンコ議論です。
このあたりは、数学をアルゴリズムと、記法をプログラミング言語と読み替えればよくわかってもらえるのではないかと思います。アセンブラの方がシンプルで一つ一つのステップは見えやすいかもしれませんが、それぞれのプログラミング言語が持っている複雑な機能や記法はあるタイプのアイデアを美しく表現するために作られていて、それなりの必然性があるのだと思います。そして、それらをコンパイルしてアセンブラで読むというのはあまり賢くない選択でしょう。
すごい人たちの直感を侮るべきではないかと
一般に教科書や論文に書かれていない細部と言うのは
1) 紙面を節約するために書かない。
2) 細部に埋没して分かりにくくなるから書かない。
3) めんどくさいから書かない。簡単だと思うから書かない。が、あるんだけど、もし良いシステムができれば(1)と(2)は撲滅できる。これだけで検証者や学習者にとってどれだけ助けになることか。とくに学習者にとっては場合によっては何倍もの効率向上になりうると思う。著者自身も自分を納得させるために論文などに書かれた分の何倍ものメモをもっている訳で、これを読者に届けないのは単に(1),(2)の問題だった。それがどれだけ読者を助けることか。
一方(3)は私もあえて撲滅するべきとは思わない。というかこれを強制するとシステムを使う人がいなくなってしまうでしょう。
これは多分違うのではないかと。すごい人たちの直感というのは本当にすさまじいし、頭の中でちょっと考えるだけで確信できる範囲が広いです*2。もちろん質問すると少し考えながら証明を教えてくれるわけですが。だから、ほとんどの場合書かない理由は(3)だと思います*3。
それに、論文の場合には最低数ヶ月、長ければ10年以上その問題について考えているわけで、基準がずれるのはどうしても仕方がないです。下手すると、数ヶ月かけて思いついた証明がtrivialに思えて仕方がなかったりするわけですから。
もっとも…
萩谷先生は否定的ですが、もしかしたら将来machine readableな証明が論文提出に必須になる可能性もあるだろうと思っています。そうなったときのために少しずつ勉強しておかないとな、とは。その前に今後数年間の競争に勝ち抜かないといけないのでそちらが先ですが。
続く…
多分。
