第1章　Mathelia

Matheliaは堅牢な数学を作成するためのソフトです。
数学を書くための記法、本として読ませる表現、証明を確かめる仕組み、が一つにまとまっています。
数学作成時の使い方の基本は 数学を書く → 表示を確認する → 機械に査読してもらう の繰り返しとなるでしょう。

★この tutorial（0_tutorial_jp）は人間向けの簡易版で、Matheliaの重要部だけを説明するものです。AI 用の tutorial（0_tutorial_AI）により多くのより細かい説明があります。
★仕様の説明では正確さに欠けたり定義が無かったりする事がありますが、その場合にはなるべく良い例を挙げます。また、tutorialは実際の本をいきなり読んでからでも悪くないと思います。
★Matheliaの仕様はまだ未確定のものも多いです。使用された方からの「こういう機能が欲しい」という建設的な意見をお待ちしております。

1.1 MatheliaとBook

数学はBookというものに書かれます。 .bookファイル に記録され、表示ソフトで閲覧されます。
自分でBookを書くには、「フォルダ一覧」の一覧のページで「ファイル操作」をクリックして新しい .book を作ります（ログインが必要）。
Bookには通常、数学記号の紹介や定義、定理とその証明、などデータが書かれていきます。
データには 証明(prf) など、表示に出ないものもあります。これはBookをスマートにするためです。

Bookは .bookファイルの仕様 に従って書かれねばなりません。
それはヘッダと本文からなり、両者は --- という行で区切られます。ヘッダと本文の各行は原則として命令語で始まります。
この行（ソース22行目）は txt という命令語で始まっています。命令語の一覧は AI用のtutorial にあります。
Book機能の例として、section番号を自動でつけてもらったり、他のBookをimportしデータを引き継いだり、ができます。
Bookのコンパイル時(表示をクリックした時)には「書法にエラーが無く表示ができるか？」「他ファイルの読み込みはちゃんとできるか？」などがチェックされます。

1.2 Bookの査読

Bookを表示させると、各頁の一番下に 査読（この頁） ボタンが出てきます(このBookには査読すべき対象が無いため出てきません)。
押すと、紹介査読（記号などが使う前に紹介されているか）と Thm査読（証明が正しいか）が続けて行われます。
どちらも OK が出れば合格です。ダメなときは FAIL が出ます。
Thm査読での FAIL は「証明の正しさの確認はできなかった」ということで、主張が偽だという判定ではありません。

査読はMatheliaの最も重要な機能で、文字通り「機械的に」チェックします。
それは、上から順に、そのBook（とimportされたBook）の「その位置までに紹介されたもの」に書かれていることだけで行われます。
なおtxt行は人間のための説明であり査読では無視されます。
また査読されるのは保存済みの .book です。結果は頁ごとに保存され、前の頁やimportした本の査読はやり直さずに結果を拾います。

1.3 Matheliaの部品

Matheliaは内部で独立性の高い部品を多く持っています。
〇DB (データベース)は様々なデータを保存します。
〇数学の記述においては、Formを扱う Formel、Thmを扱う Thmel が使用されます（詳しくは2.book, 3.book）。
〇Thmを査読する backend(prover+, vampire+, satallax+, hyperion) はMatheliaの心臓部と言えます。
さらに prover+ は内部に自動定理証明器 Prover9 を持ち、vampire+ は Vampire、satallax+は Satallax を持ちます。
〇Mathelia本体はファイル操作・Book操作などを行う他、各部品間の橋渡しをします。
Bookの堅牢さを保証するためには、各部品を堅牢にし、部品間の情報のやり取りの流れを明瞭にすることが大事です。