Mizar/はじめに

はじめに

近い将来、コンピュータを使って、数学の証明問題は正しいか否かが、すぐに判定できるようになるのが主流となることは間違いないと考えられています。 現在でも、様々なProof Checkerが誕生しています。しかし、使い勝手が悪かったり、汎用性の問題でなかなか普及して来ませんでした。 そのような中で、このMizarは数学の様々な分野（集合論、群論、数論、位相幾何、離散数学、etc.）を証明し形式化してきました。その定義、定理の数 は2008年8月現在、論文数1011編、著者207名、定理46506、定義8804 、証明の型756となっています。 また、システムの保守をポーランドのビャウィストク大学 (University of Białystok)、カナダのアルバータ大学、日本の信州大学で行っています。

Mizarとは

Proof checker。 プログラミング言語と同様に、厳密に数学の証明をする数式処理システムのひとつです。 数学を形式化し、ひとつの論文(article)とし、誰もがその引用ができるように作られています。

Proof Checker の構造

主に以下の構成によって成り立っており、これらが入れ子構造（ネスティング）をともなって処理し証明を行っています。 論理的に正しければ１(Ture)、間違っていると０(False)を結果として返します。内部的にこれらの、乗算によって処理をしているので、証明の中に一ヶ所でもFalseがあると、結果がFalseとなってしまいます。

型定義(一階述語論理)
 modeによって定義、このときにはexistenceのみ証明する。性質をattribute,clusterによって多様化

演算方法(一階述語論理)
 演算方法を定義する。
  数式 by 定理名;

証明手法(二階述語論理)
 証明の型。背理法、帰納法など
  数式 from 証明の型(scheme);