Mathel
当システムで数学を記述する言語がMathelです。\(\dagger\)次の例を見て下さい。
\(x \in X\)
青字のtex表記をクリックすると機械に入力するためのtxtと呼ばれるものが出てきます。
tex表記が同じでもtxtは異なることがありますので、こまめにクリックをして確認して下さい。
\(x\), \(\in\), \(X\) はwordで、上の例はFormです。
\(x\), \(X\) は特にv-Formとよばれ、集合を動く変数となります。\(\mathcal{X}\) や \(\alpha\) なども。
\(X\) はv_-Formでクラスを動く変数となります。「(クラスに)属する」を意味する \(\in\) を使った \(x \in X\) もFormです。
さらっと「文法をみたすもの」と言いましたが、正確な定義は長々としそうですよね！？
私たちは機械でシステムを作っています。
だから実用的には「会員ページでcheckをしてOKならForm」です。
一階言語への翻訳
Mathelは一階言語より大きいですが、一階言語への翻訳が定められています。内包記法も使用でき、次の規則が重要です。
cvt … \(T \in \{ x \mid P \}\) ≃ \(P\) の \(x\) に \(T\) を代入したもの
ここで \(T\) や \(P\) はFormの穴(Formが代入されるもの)です。
そして変換規則の表現内では \(x\) はv-Formではなくv-Formの穴です。
次の翻訳は内側からやる方が楽です。
\(x \in \{ y \mid z \in \{ x \mid x \in y \} \}\) ≃ \(z \in x\)
外側からだと \(\int f(x)dx=\int f(y) dy\) みたいな束縛変数の名前替えが必要になります。
なお翻訳は一通りではありません。 \(x \in X\) などデフォルトの翻訳が無いものもあります…
Thmel
Form(を一階言語へ翻訳したもの)たちの推論関係などを記述するのがThmelです。最も簡単な例は次でしょう。
\(\top\) ◀ O
このようなものをThm、◀ の左辺をgoal、右辺をsosと言います。Oは空の列です。
当システムではThmはcheckをされます。上のThmであれば、first-order theorem proverのbackend（例えばProver9）でcheckされます。
各Formはそれぞれの言語に翻訳されます。\(\top\) はProver語では $T になります。
上のThmのProver9からの返答には次が書かれています。\(\dagger\)
% Length of proof is 2.
当システムでは一階論理は仮定されます。次のThmは引っ掛かりやすいかもしれません。
\({\perp}\) ◀ \(x \neq y\)
Prop
よく使用されるFormには名前が付けられ、Propと呼ばれます。「等号の定義」として次のPropが登録されています。一般に 〇. は「〇の定義」と読まれます。
=. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
クラスの等号は \(=\) ですが、次のPropは一階言語への翻訳において使用されます。
=_. … \(X = Y \Longleftrightarrow \forall x \, ( x \in X \Leftrightarrow x \in Y )\)
「和集合の定義」 は次です。
cup. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
集合\({\tt X}\)はクラス\(\{x \mid x\in{\tt X}\}\)と同一視されますが、ここでも左辺でその処理が行われます。
一階言語への翻訳は複数の段階を経て次になります。
cup. ≃ \(\forall x \, ( x \in X \cup Y \Leftrightarrow x \in X \mathbin{\rm o\!r} x \in Y )\)
book
このシステムでは、数学の教科書を作る、論文の査読を行う、事が誰でもできます。
それはbookを作成して行われます。
bookにはword, Prop, Thm などを並べます。
word,PropなどはDBから取得したものを置くのが通常ですが、オリジナルのものを置くこともできます。
bookはsourceファイルを作成し、それをコンパイルするとweb上に表示されます。
web上には表示させないデータを蓄積することも多々あります。Thmの証明もそうです。
標準的な数種類のbookはデフォルトで準備されています。
新しいbookを始めるとき、他のbookをincludeすることができます。
book査読器はこのシステムで最も偉いソフトになります。
それは「未定義のwordがないか」「Thmの証明は正しいか」などをチェックします。
各bookは独立しており、例えば証明チェックは「そのbook内にあるものだけで通るか？」を見ます。
なお、bookには好みで「説明」を入れても良いですが、査読器では無視されます。
最低限の説明は以上です。
ぜひ最初のbookをご覧下さい。
ほとんどは読めば分かるはずです！？そして分からないところはAIエージェントに聞くのが基本です。
また、bookを自分で作成するときはAIエージェントに指示を出しながら行います。
私達の理想像の中核は「誰もが数学を作れること」です。そして門戸を広げても厳密さは下げません。
誰もが数学をbookとして組み立て、数学的な正しさをbook査読器が支える。難しい制作工程にはAIエージェントが伴走する。
これは単なる教科書作成システムではなく、数学の創作と検証を広く開くための基盤です。