Loading article…
Mizarシステムは、数学の定義と証明を記述するための形式言語、この言語で記述された証明を機械的にチェックできる証明支援システム、および新しい定理の証明に使用できる形式化された数学のライブラリで構成されています。 [ 1 ]このシステムは、以前は創設者であるAndrzej Trybulecの指揮下にあったMizarプロジェクトによって維持および開発されています。
2009年当時、ミザール数学ライブラリーは、厳密に形式化された数学の最大の体系的集積物であった。[ 2 ]
ミザール・プロジェクトは、1973年頃にアンジェイ・トリブレツによって、コンピュータで検証できるように数学の日常語を再構築する試みとして開始されました。 [ 3 ]現在の目標は、ミザール・システムの継続的な開発に加えて、現代数学の中核の大部分を網羅する、形式的に検証された証明の大規模なライブラリを共同で作成することです。これは、影響力のあるQEDマニフェストと一致しています。[ 4 ]
現在、このプロジェクトはポーランドのビャウィストク大学、カナダのアルバータ大学、日本の信州大学の研究グループによって開発および維持されています。Mizar証明チェッカーは依然としてプロプライエタリですが[ 5 ] 、 Mizar数学ライブラリ（検証対象の膨大な形式化された数学の集合）はオープンソースとしてライセンスされています[ 6 ] 。
ミザールシステムに関する論文は、数学形式化分野の学術コミュニティが発行する査読付き学術誌に定期的に掲載されている。これらの学術誌には、『Studies in Logic, Grammar and Rhetoric』、『Intelligent Computer Mathematics』、『Interactive Theorem Proving』、『Journal of Automated Reasoning』、『Journal of Formalized Reasoning』などが含まれる。
ミザール言語の特徴は、その読みやすさです。数学のテキストによくあるように、古典論理と宣言的なスタイルに基づいています。[ 7 ]ミザールの記事は通常のASCIIで書かれていますが、この言語は数学の専門用語に十分近いように設計されているため、ほとんどの数学者は特別な訓練なしでミザールの記事を読んで理解できます。[ 1 ]それにもかかわらず、この言語は自動証明チェックに必要な形式性を高めることができます。
証明が認められるためには、すべてのステップが基本的な論理的議論によって正当化されるか、または以前に検証された証明を引用することによって正当化されなければならない。[ 8 ]このため、数学の教科書や出版物で通常見られるよりも高いレベルの厳密さと詳細さが求められる。したがって、典型的なミザール論文は、通常のスタイルで書かれた同等の論文の約4倍の長さになる。[ 9 ]
形式化は比較的手間がかかるが、不可能なほど難しいわけではない。システムに慣れれば、教科書のページを正式に検証するのにフルタイムで約1週間かかる。これは、その利点が確率論や経済学などの応用分野にも及ぶことを示唆している。[ 2 ]
ミザール数学ライブラリ（MML）には、著者が新たに執筆した論文で参照できるすべての定理が含まれています。証明チェック担当者によって承認された後、適切な貢献とスタイルについて査読プロセスでさらに評価されます。受理された場合は、関連する形式化数学ジャーナル[ 10 ]に掲載され、MMLに追加されます。
2012年7月現在、MMLには241人の著者による1150の記事が含まれています。[ 11 ]これらには合計で10,000を超える数学的対象の形式的な定義と、これらの対象について証明された約52,000の定理が含まれています。180を超える名前付きの数学的事実がこのようにして形式的にコード化されています。[ 12 ]いくつかの例としては、ハーン・バナッハの定理、ケーニッヒの補題、ブロウワーの不動点定理、ゲーデルの完全性定理、ジョルダン曲線定理などがあります。
この幅広い範囲により、一部の研究者[ 13 ]は、ミザールを、すべてのコア数学をコンピュータで検証可能な形式でエンコードするというQEDのユートピアへの主要な近似の1つとして提案している。
MML のすべての記事は、Journal of Formalized Mathematicsの論文としてPDF形式で入手できます。[ 10 ] MML の全文は Mizar チェッカーとともに配布されており、Mizar の Web サイトから無料でダウンロードできます。進行中の最近のプロジェクト[ 14 ]では、ライブラリは実験的なwiki形式でも利用可能になりました[ 15 ] 。この形式では、編集は Mizar チェッカーによって承認された場合にのみ許可されます。[ 16 ]
MMLクエリWebサイト[ 11 ]は、MMLの内容に対する強力な検索エンジンを実装しています。他の機能の中でも、特定の型や演算子について証明されたすべてのMML定理を取得できます。[ 17 ] [ 18 ]
MMLはタルスキ・グロタンディーク集合論の公理に基づいて構築されています。意味論的にはすべてのオブジェクトは集合ですが、この言語では構文的に弱い型を定義して使用することができます。たとえば、集合の内部構造が特定の要件リストに準拠している場合にのみ、集合はNat型であると宣言できます。このリストは自然数の定義として機能し、このリストに準拠するすべての集合の集合はNATと表記されます。[ 19 ]この型の実装は、ほとんどの数学者が記号を形式的に考える方法を反映し、コード化を効率化することを目指しています。 [ 20 ]
Mizar Proof Checker の主要なオペレーティングシステム用の配布版は、Mizar プロジェクトの Web サイトから無料でダウンロードできます。この証明チェッカーは、非商用目的であれば無料で使用できます。Free Pascalで記述されており、ソースコードは GitHub で公開されています。[ 21 ]