Mathel
当システムで数学を記述する言語がMathelです。\(\dagger\)私たちは「分かりやすさ」「表現力の高さ」を追求しその開発をしています。次の例を見て下さい。
\(x \in X\)
青字のtex表記をクリックすると機械に入力するためのtxtと呼ばれるものが出てきます。
tex表記が同じでもtxtは異なることがありますので、こまめにクリックをして確認して下さい。
よく使用されるFormには名前が付けられ、Propと呼ばれます。
「等号の定義」として次の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 \}\)
Mathelは一階言語より大きいですが、一階言語への翻訳が定められています。
Thmel
Form(を一階言語へ翻訳したもの)たちの推論関係などを記述するのがThmelです。最も簡単な例は次でしょう。
\(\top\) ◀ O
このようなものをThm、◀ の左辺をgoal、右辺をsosと言います。
sosは一般には列ですが、Oは空の列です。
Thmの各FormがProver語に翻訳されてから送られます。\(\top\) は $T になります。
Prover9からの返答はoracleと呼ばれ、この場合は
% Length of proof is 2.
などと書かれています。証明終了です\(\dagger\)
\({\perp}\)◀ \(x \neq y\)
は引っ掛かりやすいかもしれません。なお {/} は否定を作っています。
以上でライブラリを読むための最低限のルールが終わりです。
ライブラリではwordやThmなどを蓄積しており、ほとんどは読めば分かるはずです！？
分からないところは全てAIエージェントに聞くのが基本です。
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.
ここで W. は記号の定義を集めた列です。
W. は無限列なので上のThmをProver9に送ることは不可能です。
一般にProver9用にThmを変形することはprepと言われます。
`X cup X = X` ◀ =. , cup.
とprepされるべきですね？これで得られるoracleには次が書かれます。
% Length of proof is 16.
さて、実はこれは良いprepではありません。
私たちのAIなら、この定理は「定義を使った変換」だけで自明な式になる、と予想するはずです。
それはslash計算と呼ばれ
/ 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の探索空間は劇的に狭まります。
なお証明では「同値な式の置き換え」に関する一階論理の定理も使用されていることになります。