まえがき


かねてから数学がより美しくまたあいまいさの少ない形で形式化できないものか、と考えていた。大学で数学を若い人達に教えるたびにその御都合主義的な記法にいつも後めたさを感じてきた。コンピュータのプログラム言語のように数学言語というものがきちんと定義できないものか、と考えた。

更に数学言語が完全に定式化できれば、その言語で書かれた数学に誤りがないかどうかを自動的にコンピュータでチェックできるはずである、と思われた。そうすれば数学理論の正しさのチェックが容易になり、数学者は証明をチェックしてくれる仲間を探す必要がなくなり、思いきった数学理論の展開も可能になるであろう。また未解決問題の証明を公募すれば若い天才を簡単に見出すこともできるはずである。更にまた数学が真の客観性を取り戻すことによって数学以外の分野に再び強い影響を与えることも可能になろう。

幸いこの構造は初期の目標通り著者自身の満足のゆく形で完成した。現在学生の数学教育用にこのシステムを利用しているが、学生以外の専門家の使用にも耐えるものである、と考えている。なるべく多くの人にこの数学言語を理解してもらい、できるならば東大の大型計算機センター等を通じてこのシステムを使ってもらいたい。このシステムは決して完成されたものではない。言語を設計してゆく段階で、どのように決めるべきか迷ったことが何回もある。しかし未完成の段階では人に相談することもできず、孤独な作業が続いた。ここまで完成していれば、理解してくれる仲間を増やすことができ、そしてかつて著者が一人だけで悩んだ問題を、再び今度は多勢で共に考えることができる。この解説書がそのような仲間を一人でも増やすことに役立つことを祈っている。

おわりに初期の段階で卒業研究にシステムづくりをとりあげ協力してくれた高橋裕司君に感謝したい。またこの研究のために、コンピュータが自由に利用できる環境づくりに協力してくれた私の研究室のスタッフ一同に感謝したい。

   昭和60年12月1日           長野市にて

                         中 村 八 束