第1章　例で見るMathelia

Matheliaは堅牢な数学を作成するためのソフトです。数学はBookに書き、それを機械が検査（査読）します。

Mathelia で何ができるか・何が弱いか・これから何が入るかの概観は 0.book にあります。
3つの例で、①Thm と prf、②記号の紹介と前提、③定数と前提の足りないとき、を順に見ます。どの例もこのBookに実際に書かれていて、査読を通ります。
以下では、ソースの行を説明のために このような表示 で再掲します。.bookファイルにはその行をそのまま書きます。式はバッククォート ` ` で囲んで書きます。

1.1 例1　Thm と prf

\(x = y \Longrightarrow y = x\) \(\blacktriangleleft\) O
ソース（.bookファイル）では次の2行です。
thm `x = y ⟹ y = x` ◀ O
　thm はThm（主張）を書く命令です。A ◀ Γ は「◀ の右に並べた前提の列 Γ から、左の式 A が推論できる」と読みます。A を goal、Γ を sos（set of support＝前提の集まり）と言います。
　O（大文字のオー）は空の列です。この例では ◀ の右に前提が何も無く、x = y は goal（x = y ⟹ y = x）の一部です。
　x, y は変数で、「すべての x, y について」の意味になります。
　= と ⟹ は、ヘッダの import /common/word_logic で読み込んだ Book が紹介済みの記号なので、そのまま使えます。その Book が紹介している主な記号は次のとおりです。
　　⊤（真）　⊥（偽）　¬（否定）　and（かつ。表示は「,」）　or（または）　⇒ ⇔（ならば・同値）　⟹ ⟺（結合の弱い ならば・同値）　∀ ∃ ∀_ ∃_　= =_　and_　{/}（否定。x {/}= y は x ≠ y）
　結合は、+ などの演算が = より強く、= が and より強く、and が ⟹ より強くなります（x = y and y = z ⟹ x = z は (x = y and y = z) ⟹ x = z）。迷ったら括弧を付けます。
prf `x = y ⟹ y = x` ◀ O p;
　prf は直前の Thm の確かめ方を書く所で、表示はされません。確かめ方はいくつかの段階に分けて書くこともできますが、この例は1回で済むので、Thm と同じ形をそのまま書き、末尾に投げ先を付けます。
　p; は「prover+（内部で自動定理証明器 Prover9 を使う）に投げる」という意味です。自分で証明を1歩ずつ書く代わりに、証明器に「この前提からこの式が出るか」を探させます。投げ先はほかに v; s; h; があります（3.book）。
ここまでで最小のBookが書けます。次の5行が Mathelia の「Hello World」です。まずこれを動かしてください。Bookの一覧のページ（/book_collection/）で新しいBookを作り（ログインが必要）、5行を写して保存し、査読すると OK になります。
　⟹ ◀ などの記号は Unicode の文字そのもので書くので、この頁からコピーするのが確実です（文字コードは「ファイルの基本」）。ログインせずに作業するときは、同じ内容を .bookファイルとして置いて CLI で査読します（「CLIから査読する」の章）。

1.2 例2　記号の紹介と前提

word(ss,s) … \(+\)
+結合則 … \(x + ( y + z ) = ( x + y ) + z\)
\(x + ( y + ( z + w ) ) = ( ( x + y ) + z ) + w\) \(\blacktriangleleft\) +結合則
「結合則を満たす演算なら、4つの項でも括弧を付け替えられる」という定理です。ソースでは次の4行です。
word +
　記号 + は import した Book が紹介していないので、使う前に紹介します。表示の (ss,s) は + のgramで、「s-Form を2つ受け取り s-Form を返す」＝2項演算であることを表します。gram は DB に登録されていて、紹介すると表示されます。
　ここでは + の意味（数の足し算など）は何も決めていません。分かっているのは次の前提だけです。
prop +結合則 <- `x + (y + z) = (x + y) + z`
　prop は式に名前を付けます。名前を付けただけで、証明されたわけではありません。ここでは前提として ◀ の右に置きます。x, y, z は量化子（∀ ∃）で縛られていない変数なので、前提としても「すべての x, y, z について」の結合則になります。
thm `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則
prf `x + (y + (z + w)) = ((x + y) + z) + w` ◀ +結合則 p;
　結合則を仮定しない演算では、この等式は一般には成り立ちません。実際、thm と prf の両方で ◀ の右の +結合則 を O に替えると、証明は見つからず、査読は FAIL になります。FAIL は「この前提からは確かめられなかった」ということで、主張が偽だという判定ではありません。

1.3 例3　定数と、前提の足りないとき

word(ss,p) … \(\in\)
仮定1 … \(\forall x ( x \in \mathrm{A} \Longrightarrow x \in \mathrm{B} )\)
仮定2 … \(\mathrm{a} \in \mathrm{A}\)
\(\mathrm{a} \in \mathrm{B}\) \(\blacktriangleleft\) 仮定1 ，仮定2
「A のどの元も B に属し、a が A に属するなら、a は B に属する」という定理です。ソースでは次の5行です。
word ∈
　表示の (ss,p) は、∈ が「s-Form を2つ受け取り p-Form（命題）を返す」ことを表します。例2の + は s-Form を返し、∈ は p-Form を返します。
prop 仮定1 <- `∀ x (x ∈ |A ⟹ x ∈ |B)`
prop 仮定2 <- `|a ∈ |A`
　|A, |B, |a のように | を付けたものは定数です。紹介せずに使えます。表示では | は消え、定数は立体（a）、変数は斜体（x）で示されます。
　例2で見たとおり、量化子で縛られていない（集合・クラスの）変数は、前提の中でも「すべての値について」の意味になります。仮定1 の ∀ x は省いても同じ意味ですが、読みやすさのために書いています。
　一方、仮定2 を |a ∈ |A でなく a ∈ A と書くと「すべての a, A について a ∈ A」という強すぎる前提になり、意図した定理ではなくなります。特定のものについて述べるときは定数を使います。
　前提に書いたものの意味を表にまとめます（高階変数と schema は 7.book・6.book で扱います）。

前提に書いたもの（ソース）	意味
x ∈ A（量化子で縛られていない集合・クラスの変数）	すべての x, A について（全称で閉じる）
|a ∈ |A（定数）	ある特定の a, A について
P^・?R^ を含む prop（高階変数）	Thm 全体の外側で1回だけ全称で閉じる＝goal と sos で同じ1つの命題・述語を指す（前提の中だけで閉じるのではない。式を代入して使うことはできない）
schema（schema 名(…) :=）	どの述語についても成り立つ前提。代入した実例 名[?R^:=`θ`] を段の sos に書いて使う

thm `|a ∈ |B` ◀ 仮定1 , 仮定2
　前提が2つ以上あるときは ,（前後に半角スペース）で区切ります（表示では「，」になります）。旧い ,, は査読エラーです。
prf `|a ∈ |B` ◀ 仮定1 , 仮定2 p;
　thm と prf の両方で ◀ の右を 仮定1 だけにする（仮定2 を外す）と、証明は見つからず、査読は FAIL になります。

第2章　Bookの書き方

Bookは .bookファイル に記録され、表示ソフトで閲覧されます。
.bookファイルはヘッダと本文からなり、両者は --- という行で区切られます。各行は原則として命令語で始まります（例外は、字下げして次の行に続けた prf の続きです）。上の例では thm・prf・word・prop が本文の命令語です。
ヘッダの行は次の意味です。
　title … Bookの題。author … 書いた人。
　import /common/word_logic … = ⟹ ∀ などの論理の記号を紹介済みの Book を読み込みます。書くときは .book を付けません（表示では付きます）。
　Thm・証明の扱いを決める設定ファイル（.thmel）は thmel 名前 の行で指定します。formel（式の言語の設定）・thmel とも、書かなければ /common/default になります。
保存すると、まずコンパイルで「書法にエラーが無く表示ができるか？」「他ファイルの読み込みはちゃんとできるか？」がチェックされ、表示されます。証明が正しいかは、次の査読で確かめます。

第3章　Bookの査読

査読はMatheliaの最も重要な機能で、「まだ紹介されてない記号が無いか？」「証明が正しいか」などを、文字通り「機械的に」チェックします。
それは、上から順に、そのBook（とimportされたBook）の「その位置までに紹介されたもの」に書かれていることだけで行われます。なおtxt行は人間のための説明であり査読では無視されます。
Bookを表示すると、各頁に「査読（この頁）」というボタンが出ます。押すと、紹介査読（語・prop などが使う前に紹介されているか）と Thm査読の結果が「紹介査読：…」「Thm査読：…」の2行で続けて出ます（下にまとめの1行はありません。まとめの総合判定は下の CLI が出します）。ヘッダに option review quick:true; と書いた本には「簡易Thm査読（この頁）」も出ます。結論のつなぎ（Hyperion）などを省いた速さ優先の Thm査読で、prf を試すときに使います（その OK は〇の根拠にはなりません）。Thm査読の表には Thm ごとに番号（#1.2-1 は 1.2 節の1番目の Thm。subsection の前にある Thm は #1-1 のように節番号だけ）と結果（通れば処理時間を添えた OK＝例 0.12秒 OK、落ちれば FAIL と理由）が並んで表示されます。
FAIL は査読に通らなかったことを示します。理由には、証明が見つからない場合（例2・例3の前提を外したとき）のほか、未紹介の記号を使った場合などがあります。例えば例2で word + の行を消すと、「本が紹介していない word を Form の中で使っています: +」という理由で FAIL になります。
　CLI での査読結果は、例えば次のような行で返ります（Thm の番号・Thm または ファイル:行・結果）。
　#1.1-1　\(x = y \Longrightarrow y = x\) ◀ O　0.12秒 OK
　#1.2-1　1.book:33　FAIL: 本が紹介していない word を Form の中で使っています: +
　DB に無い記号を word で紹介しようとすると、査読より前のコンパイルの時点で「word は言語に無い綴りです: ♠」のようなエラーになり、表示もできません。
FAIL のときは理由を読み、記号を紹介する・前提を足す・証明を段に分ける（3.book）などをしてから、保存し直して再び査読します。
査読されるのは保存済みの .book です。結果は頁ごとに保存され、前の頁やimportした本は、中身が変わっていなければ査読し直さず、保存された結果を使います。

第4章　CLIから査読する

ブラウザの査読ボタンを押せない場合（AIエージェントが対話画面を持たずに作業しているときなど）は、Web画面の「査読」ボタンと全く同じ査読（紹介査読と Thm査読）をCLIから実行できます。

<本の名前>はフォルダ名/本の名前（拡張子なし。例 articles3/1）。頁番号は1から数え、省略すると本全体を査読します（「option review per-page:false;」を宣言した本では頁番号は効きません）。Webのエディタでも編集できるように、置いたファイルはグループを www-data、パーミッションを 664 にしておきます。
実行すると、紹介査読の件数（落ちた行があれば行番号と理由）、各Thmの番号・結果（OK／FAIL、FAILなら理由）、全体の判定（例 総合判定: ALL OK（紹介査読 OK／Thm査読 OK））をプレーンテキストで返します。終了コードは0＝ALL OK、1＝紹介査読か Thm査読に FAIL あり、2＝引数や本の指定の誤り、3＝判定できない（コンパイルエラーなど。総合判定は「不明」）です。--inputs を付けると、FAIL した行の下に、落ちた段について prover+ などが受け取ったもの（翻訳した後の式）と、証明器へ投げた入力を、この順に出します（読み方は 3.book）。分割したときは入力が複数並び、1本ごとの結果（# 1/3 の結果：timeout など）と、受理の条件（全部が proved なら認める）の集計も出ます。成功した段の入力は出しません。どの定義が開かずに残ったかなど、FAIL の原因を読むのに使います（practice.book）。式の読まれ方や slash の書き換えだけを確かめるときは、証明器に投げない次のコマンドを使います（2.book・4.book）。

式だけを書くと読まれ方（前置記法）が、// W. などを付けると書き換えた結果が返ります。自分で書いたThmが正しいかを確かめるのは、上の review_cli です。
DB の prop の本文は '`@名`' で見られます（例 slash_cli.php articles3/0 '`@+𝕄`'）。import する本にどんな定理があるかは、表示しない !let/thm などの補題も含めて、grep -nE '^!?(thm|prop/thm|let/thm)' wp-content/themes/lightning/mathelia/articles3/0.book で一覧できます。表示しない補題も、import した本から使えます。
prf を探すときは、1つの Thm に prf の候補をいくつも当てて比べられます（本は書き換えません。外の AI も使ってかまいません）。

候補ごとに、通ったか・失敗した段・PHP と証明器の秒を JSON で返します。候補に = と書くと今の prf を測ります。--quick は結論のつなぎ（Hyperion）を省いた速い試しで、その ok は〇の根拠になりません。通った候補は本に書いて review_cli で確かめます。
対象の Thm は、thm の行の行番号でも、その行の一部の文字列（一意に決まること）でも指せます。prf_trial は候補ごとに一時的な本を同じフォルダに作り、終わると消します。本の名前は拡張子なしで渡します（.book を付けても読めますが、表示が .book.book になります）。

第5章　次にすること

・例1の5行のBookに、例2・例3を書き足してみてください。
・ログインせずに作業するとき（AIエージェントなど）は、.bookファイルを /var/www/test2.atp-research.com/wp-content/themes/lightning/mathelia/フォルダ/名前.book に置き、上の「CLIから査読する」のコマンドで査読します。
・続きは 2.book（式の書き方 Formel）、3.book（Thmと証明 Thmel）、4.book（高度な表現）、5.book（ものとクラス）、6.book（集合とクラス）、practice.book（実践：投げ先・失敗・戦略）へ。高階変数と schema は 7.book にあります。

★Matheliaの仕様はまだ未確定のものも多いです。使用された方からの「こういう機能が欲しい」という建設的な意見をお待ちしております。

第6章　Matheliaの部品

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

第7章　ファイルの基本

.bookファイルは文字コード UTF-8（BOM なし）で書きます。改行は LF でも CRLF でも構いません。
　Shift_JIS などで保存すると「UTF-8 ではない文字があります」、BOM 付きの UTF-8 で保存すると「先頭に BOM があります」というコンパイルエラーになります。⟹ ◀ などの記号は Shift_JIS では表せません。
記号は Unicode の文字そのもの（⟹ ∀ ∈ ◀ など）で書きます。これらの記号の以前の ASCII の綴り（==> all in など）は使えません。
変数は英字1文字に数字や ' を付けたもの（x, A, x1, x'）とギリシャ文字（α, α1）などです。定数はその前に | を付けたもの（|a, |A1）です。
フォルダ名・Book名には半角の英数字と _ - を使います（例 0_tutorial_AI/1）。
1行に1つの命令を書きます。長い prf だけは、次の行を字下げして続けられます。
見た目が似ていても別の文字です。取り違えたときに出るエラーも挙げます。
　⟹ と ⇒ … どちらも Formel の記号で、結合の強さが違います（2.book）。取り違えてもエラーにならないので注意します。
　半角スペースと全角スペース … 命令語の後が全角だと「Unknown line kind」、式の中だと「この Formel の語でも変数・定数の綴りでもありません」。
　`（バッククォート）と ‘ … thm で ‘ を使うと「‘式‘（一階言語の式）は txt 行だけで使えます」。
　∈ と ε … ε はギリシャ文字の変数になり、「「ε …」が余っています」。
　◀ と ◁ … prf で ◁ を使うと「prf の段に書けない演算子です: ◁」。
　-| の - と − （マイナス記号 U+2212）… thm で − を使うと「「−」（U+2212 マイナス記号）が使われています」。
　, と ，・、 … 前提の区切りに ， や 、 を使うと「前提（sos）の区切りは半角の , です（前後に空白）」。旧い ,, や前後に空白の無い , も、その Thm の査読エラーになります。
　O（大文字のオー）と 0（ゼロ）… ◀ 0 は「unintroduced sos name: 0」。
　∅ と Ø … Ø は「この Formel の語でも変数・定数の綴りでもありません」。