Mathel
当システムで数学を記述する言語がMathelです。\(\dagger\)次の例を見て下さい。
\(x \in X\)
青字のtex表記をクリックすると機械に入力するためのtxtと呼ばれるものが出てきます。
tex表記が同じでもtxtは異なることがありますので、こまめにクリックをして確認して下さい。
\(x\), \(\in\), \(X\) はwordで、上の例はFormです。
Mathelには多くの省略記法が用意されています。例 \( x , y \in X\) ≈ \(x \in X , y \in X\)
Mathelは一階言語より大きいですが、一階言語への翻訳が定められています。
例えば、否定を作るword関数 {/} というものがあり、 \(x \notin X\) ≃ \(\neg ( x \in X )\)
txtにおいて半角スペースはwordの区切りを意味しますが ( ) の前後では略せます。
クラスを動く変数 \(X\) とクラスに「属する」を意味する \(\in\) を使った \(x \in X\) もFormです。
これは一階言語への翻訳がerrorになります…
Thmel
Form(を一階言語へ翻訳したもの)たちの推論関係などを記述するのがThmelです。最も簡単な例は次でしょう。
\(\top\) ◀ O
このようなものをThm、◀ の左辺をgoal、右辺をsosと言います。
sosは一般には列ですが、Oは空の列です。
Thmの各FormがProver語に翻訳されてから送られます。\(\top\) は $T になります。
Prover9からの返答はoracleと呼ばれ、この場合は
% Length of proof is 2.
などと書かれています。証明終了です\(\dagger\)
次の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 )\)
Mathelでは内包記法も制限無く使用できます。「和集合の定義」 は次です。
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 )\)
最低限の説明は以上です。
ぜひライブラリをご覧下さい。
ライブラリではword, Prop, Thmなどを蓄積しており、ほとんどは読めば分かるはずです！？
そして分からないところはAIエージェントに聞くのが基本です。
なおライブラリでは、記述は淡々と行われ、記号の意味や読み方を与えたり親切に説明をすること等は基本的にありません。
さらっと「文法をみたすもの」と言いましたが、その説明ってとても長くなりそうですよね？
私たちは機械でシステムを作っています。
だから本当は「会員ページで実行できるチェックをしてキチンと結果が返ってくるものがForm」です。
AIによる証明
当会のAIエージェントはclaudeで
①web上のデータを大量に学習をしており、大学レベルの数学をこなす能力があります。
②当システムの仕様も学習しており、システムの道具を使いこなす能力もあります。
証明は ①数学知識を基に予想 → ②システムで確認 という流れで作られます。
難しい定理では試行錯誤は必要になりますが…
兎にも角にも、AIによる証明を体験して下さい。集合論の基本結果を使って練習してみましょう。
例 \(X\cup X = X\)
X U X ＝ X を証明して
と入力してみて下さい。AIは正しく
X cup X = X
とMathelへの翻訳をしてくれる可能性が高いです。
AIはこの定理の証明に何が必要か？考え、「各記号の定義があればよい」と判断します。
`X cup X = X` ◀ W.
ここで ` はFormをPropにする記号、W. は記号の定義を集めた列です。
W. は無限列なので上のThmをProver9に送ることは不可能です。
一般にProver9用にThmを変形することはprepと言われます。
`X cup X = X` ◀ =. , cup.
とprepされるべきですね？これで得られるoracleには次が書かれます。
% Length of proof is 16.
さて、実はこれは良いprepではありません。
私たちのAIなら、この定理は「定義の展開」だけで自明な式になる、と予想するはずです。
/ W. で =. が使われ \(\forall x .\,(x \in X \cup X \Leftrightarrow x \in X)\)
さらに / W. で cup. が使われ \(\forall x .\,((x \in X\,{\rm o\!r}\,x \in X) \Leftrightarrow x \in X)\)
となります。このような文字列処理も機械は得意です。AIは
`X cup X = X` // W. ◀ O
とprepするでしょう。// W. は / W. / W. のことです。これだとoracleには次が書かれます。
% Length of proof is 6.
システムでも推論をすることでProver9の探索空間は劇的に狭まります。