設立主旨
数学はかつて科学における女王のような立場にありました。ガウスのように、数学者は同時に科学者でありまた天文学者でもありました。ニュートンはライプニッツと並んで微積分学の創始者であると同時に勿論、力学の祖でもあります。しかし２０世紀になって公理主義が力を持つと同時に（それは相対性理論など新しい物理学に適切な数学を提供できた、という功績はありましたが）、数学者の数だけ公理系がある、というような状況になり、数学は発散と孤独化の道を歩み始めます。当然のように科学者や工学者は現代数学を理解できなくなり、そして数学を無視しはじめます。それが現代数学の病因だと考えられます。しかし他方、２１世紀になり、コンピュータ化した時代には、益々高度の数学が要求されます。
私の大学での恩師梅垣寿春教授は、「第一次大戦は化学の戦争であった。火薬、毒ガス、などは化学の産物である。第二次大戦は物理学の戦争であった。航空機、レーダ、原爆などは物理学の産物である。もしこれから第三次大戦が起きれば（起きては困るが）それは数学の戦争であろう」、と日頃話しておられまし た。それは何十年も前の話なので、そんなことがあり得るのだろうか、と私は疑問に思いながら聞いていたものです。
しかしコンピュータの発達した現代ではそれは真実味を帯びています。ミサイルは優れたナビゲーションソフトによって制御されています。暗号は高度の代数学を使って作られます。ロボット兵器は人工知能ソフトによって動かされています。第三次大戦など起きないとしても、国際的な経済戦争はやはり、数学を利用した高度のコンピュータシステムが主役になるでしょう。
コンピュータは、高度かつ精緻な数学の要求者であると同時に、そのような新しい数学手法の生みの親でもあるのです。即ち、プルーフチェッカーと数学言語の出現を可能にしました。もっと端的に言えばMizarの出現を可能にしたのです。MizarはポーランドのTrybulec先生が中心になって開発されたシステムです。Mizar言語で書かれた数学理論は、Mizarのチェッカーソ フト（verifier）によってその正しさが自動的にチェックされます。チェックを通った理論は（その他のチェックもありますが）インターネットのサー バに置かれ（Mizar Mathematical Library、MML）、人類共有の知的財産として世界に公開されます。
Mizarの知的財産は不思議な性格を持っています。誰でもが（国籍、貧富、性別、年齢、階級などに無関係に）只で入手可能な、公平な財産です。でもそれを重要視しない人々にとっては何の良いこともありません。しかし重要視する人々には力や富や繁栄を与えることができます。Mizarライブラリーへの日本の貢献は大きなものがあります。これは最も崇高なボランティア的活動であり世界に貢献すると同時に、日本自身の科学技術の水準をトップランクに押し上げうるものです。Mizarの日本に於ける活動が益々重要になるにつれ、日本に於ける研究者がもう少し組織化されて、社会に影響を及ぼせる形にすべきと考えます。
それが「日本Mizar学会」設立の主旨であります。この学会は単にMMLを増やす活動だけでなく、ガウスの時代のように高度な新しい数学が、科学や技術や産業に重要な影響を及ぼせるような活動もしてゆきます。この学会を基盤にして、個々の研究者は生き生きとした活動を始められることでしょう。
２００７年５月１日 中村八束
