当研究会ではAIを利用します。
それは当会のエージェントとしてカスタマイズされたclaudeで
①web上のデータを大量に学習をしており、大学レベルの数学をこなす能力があります。
②当システムの仕様も学習しており、システムの道具を使いこなす能力もあります。
以下、初心者向けに当会のAIによる証明のチュートリアルをします。
例① \(x = x\)
まず、自明な例で流れをつかみましょう。チャット画面で、次のように入力するだけです。
x = x を証明して
当システムではMathelという言語で数学を記述しますが x = x はそのままMathelになります。
AIは「この定理は自明である」と判断し、次を作成します。
`x = x` ◀ O
この形のものはThmと呼ばれます。一般に◀の右辺は列ですが、Oは空の列です。
当システムではThmが正しいかの判断をProver9に任せます。
Thmの各式がProver語に翻訳されてから送られます。x = x はProver語でもそのままです。
Prover9からの返答はoracleと呼ばれ、この場合は
% Length of proof is 3.
などと書かれています。証明終了です！
Prover9も無償のソフトですので、気になる方は直接確かめてみて下さい。
例② \(X\cup X = X\)
集合論の基本結果を使って練習してみましょう。
X U X ＝ X を証明して
と入力してみて下さい。AIは正しく
X cup X = X
とMathelへの翻訳をしてくれる可能性が高いです。
AIはこの定理の証明に何が必要か？考え、「各記号の定義があればよい」と判断します。
`X cup X = X` ◀ W.
ここで W. は記号の定義を集めた列です。
「= の定義」は =. とされ、次の式が登録されています。
\(X = Y \Longleftrightarrow \forall x \, (x \in X \Leftrightarrow x\in Y)\)
Mathelでは内包記法も自由に使用でき cup. は次です。
\(X \cup Y = \{x \mid x \in X \,{\rm o\!r}\, x \in Y\}\)
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. / W. ◀ O
とprepするでしょう。これだとoracleには次が書かれます。
% Length of proof is 6.
システムでも推論をすることでProver9の探索空間は劇的に狭まります。
なお証明では「同値な式の置き換え」に関する一階論理の定理も使用されていることになります。
他の機械数学システムとの違い
Lean, Mizar, Coq, Isabelleなどの他の機械数学システムでは、証明の形式化を行います。
数学者が普段書くような証明を機械が検証できる形式的な言語に翻訳する作業です。
例えば
…
当研究会では形式化を行いません。
人間は何を証明したいかだけを書けば、あとは自動で証明が作成されます。