中学生になると、数学に図形問題というのが、あらわれる。三角形の相似性の証明とか、そういったやつだ。線Ａと線Ｂが平行であることを証明せよ、みたいなやつだ。
なんだか分かんないけど、教科書に書いていることを真似て、いろいろいじくっていると、答が書ける。でも、この証明ってやつは、なんだろう？ 急に現れた「なにか」。
証明とは、この数学体系内における、一つの「変換」生成ログ、である。数学体系にしても、なにもないところから、なにかを生みだすことはできない。あくまで、ある「条件」、ルールが、その規制の範囲で、
活動
する。つまり、そのトレースログが証明といえる。人間の活動が当然その物理系の範囲内にあり、そのライフログが存在するのと同じことだ。
証明問題とは、その逆方向の「遡行」を、帰納することを目指すゲームといえるだろう。
よく考えれば、小学校から行っていた、算数も、すべて、問題は「証明」であった。それを証明として、体裁を整えなかったのは、直感的に分かりづらかった、くらいの意味しかないだろう。
そうなってくると、とたんに、証明ってなんなのかな、って気になってくる。なにがどうなっていることが、証明なのだろう？
いや。質問を変えよう。どうして、多くの子供たちは、普通、学校で試験で、数学の問題を解くとき、この問題で悩まないのか、と。
それを一言で言うなら、それが「具体的」だからと言えるだろう。
そういった場合において、「分かって」答を書く段階になったとき、書くべき情報は、ほぼ自明だからである。幾つかのポイントが書いてあれば、「この学生は分かっている」として、先生は満点をつける。
つまり、大事なことは、ここでの「証明」とは、言わば、授業における、先生と生徒の相互作用の「延長」における、生産物であることが、自明の前提とされている、ということだ。
つまり、証明とは一種の「説得」である、ということである。ここは、科学論のポイントでもある。学術論文がレフェリーにジャッジされるとき、ようするに、レフェリーが納得したかどうかが、評価されるかされないかの、唯一の分岐点である。こう言うと「なんでもあり」に思えるかもしれないが、その学問内において、さまざまな共通の前提が存在することが「自明の前提」とだれもが思っているから、ここにおいては、重要視されるのは、証明ではなく、
「複数の」ジャッジによる承認
の事実性となる。
そんな、いいかげんな、と思うかもしれない。しかし、実際にレフェリーはその道のプロですから、それほど外れた結論を出さないわけで、実際、この結果に紐付く多くの応用コンテンツが生成されれば、だれでも、その結果を認めざるをえなくなるわけで、そう考えるなら、それなりに信用を置けるシステムといえる。
しかし、こと、数学に限るならば、これは「機械化」できるんじゃないのか、と、たいていの人は思うのではないだろうか。実際、同じようなパターンで証明は記述されるわけですし。
そして、この直感は正しい。それが、数学基礎論なのだが、カントールの直感的集合論も、（いびつな形ではあったが）公理的に形式化されたわけだ。
しかし、もし、形式化が成功したのなら、その次のステップはなんだろう。もちろん、
プルーフチェックの機械化。
つまり、これによって、記述した証明（プログラム）が「正しい」（走らせたプログラムのリターンが正常終了）ことを、確認してしまうのだ。
どうだろう。
数学の好きだった子供なら、もし、こんなものがあったらいいなーと思ったことが、一度はあるんじゃないだろうか。
というか、ある。
Mizar の配布物には、新たに書かれる Mizar-論文で参照可能な種々の定義および定理から成る Mizar 数学ライブラリ (Mizar Mathematical Library, MML) が含まれる。レビューと自動検証を受けた新たな論文は、形式化数学ジャーナルの関連刊行物で公表することができ、また然る後 MML の一部に組み込まれる。
以前、ちょっとハマったときがあって、いろいろ、さわってみたけど、別に、自分でもいろいろ証明を書いてチェッカーを動かしてみたが、普通にやれた（マニュアルが貧弱ではあったが）。ただ、やってみると分かるけど、人間が直感的にやってる、メタの議論を、一つ一つ記述をしないといけないんで、簡単なことをやることが、逆にうざかったりする。
その辺りが、ライブラリ化作業がなかなかスピードが遅く、少しづつ進んでいる理由なのだろうか（いろいろ技術的な課題もあるのだろうか...）。
昔からあるプロジェクトのようで、正直、あまり、扱いやすいプログラムじゃない。こういった「プログラム」の集積が、もしかしたら、かなりの（ＩＴ業界などの）資産にならないかな、と思ったこともあるが、いずれにしろ、個人的な、興味は大きい（これを使って、数学の本を読んでいて、証明が分かりづらかった場合とか、簡単にこのソースの該当個所を確認して、分かる、なんていう使い方ができたらいいですよね）。
別に、このプロジェクトじゃなくても、なんでもいいんだけど、いずれにしろ、もっと使いやすいようになってくれないと、なんともはや、ということでしょうか。
