Form文法の始め
ほとんどのwordはbookで「紹介」されます。例えば\(\mathbb{W}_0\)(ss,p) … \(\in\) \(=\)
\(\mathbb{W}_1\)(sc,p) … \(\in\)
\(\mathbb{W}_1\)(cc,p) … \(=\)
この (ss,p) はgramと呼ばれます。gramに現れる型には v,s,c,p などがあります。\(\dagger\)
Formにはs-Form, c-Form, p-Formがあります。
v-Formは特別なs-Form、v_-Formは特別なc-Form、v^-Formは特別なp-Formです。
\(x \in X\) や \(x \in X\) はp-Formです。
wordは紹介時に表記法が付くことがあります。
例えば表記法がFのword \({\tt w}\) は \({\tt w}\)(\({\tt x}_1\), …, \({\tt x_n}\)) の形で使用されます。
略記Form
例えば次の略記が使えます。 \(x , y \in X\) ≈ \(x \in X , y \in X\)bookではabbr(略記法の規則)も紹介されます。上の略記に対しては
abbr … \(X_{1} , \cdots , X_{\tt n} \mathop{{\sf A}}\) ≈ \(X_{1} \mathop{{\sf A}} , \cdots , X_{\tt n} \mathop{{\sf A}}\)
\(\cdots\) や \({\tt n}\) はしかるべく処理されます。
wordとabbrがセットになることもあります。1以上の自然数 \({\tt n}\) に対して
\(\mathbb{W}_0\)(s\(^{\tt n}\),s)F … \(\mathsf{set}_{\tt n}\)
abbr … \(\{ x_{1} , \cdots , x_{\tt n} \}\) ≈ \(\mathsf{set}_{\tt n} ( x_{1} , \cdots , x_{\tt n} )\)
ただし s\(^{\tt n}\) は s を\({\tt n}\)個並べたものです。
ほとんどの場合略記が使用され、右辺の形は機械内部でしか見られないでしょう。
Thmの証明
book中で使用される変数があります。
最も重要なのは \(\mathbb{W_0.}\) です。これは、bookの中で、そこまでで紹介された \({\tt w}.\) (\({\tt w}\)は\(\mathbb{W_0}\)) のすべての列です。
Thmとそのcheckの例
記号の定義を集めた列を \(\mathbb{W}_0.\) とします。次のようなThmはよく現れます。\(X \cup X = X\) ◀ \(\mathbb{W}_0.\)
\(\mathbb{W}_0.\) は無限列なのでこれをProver9に送ることは不可能です。どの定義を使っているか具体的に書いて
\(X \cup X = X\) ◀ =. , cup.
をProver9に送ると、次が返ってきます。
% Length of proof is 16.
=. , cup. ◀ \(\mathbb{W}_0.\) というThmは、メタ推論を行うHyperionというソフトでcheckされます。
/ \({\tt w}\). は「\({\tt w}\)の定義による展開」を行います。
\(X \cup X = X\) / =. = \(\forall x \, ( x \in X \cup X \Leftrightarrow x \in X )\)
\(X \cup X = X\) / =. / cup. = \(\forall x \, ( x \in X \mathbin{\rm o\!r} x \in X \Leftrightarrow x \in X )\)
\({\tt P}\) ◀ \(\mathbb{W}_0.\) の証明では、次の3つのThmをcheckとする戦略が優秀です。
\({\tt P}\) / \({\tt w}\). ◀ O
\({\tt P}\) ◀ \({\tt P}\) / \({\tt w}\). , \({\tt w}\).
\({\tt w}\). ◀ \(\mathbb{W}_0.\)
1番目のThmをProver9で、2,3番目はHyperionでcheckします。
\(X \cup X = X\) / =. / cup. ◀ O
の方がProver9にとっては簡単で、次が返ってきます。
% Length of proof is 6.
Thmのcheck
Thmのcheckを行う部分は当システムで最も注意深く開発が行われています。
私達は「Thmが正しいか」について人類を超越したレベルの検証をしようとしています。
どれだけ細かい人でも、長大な証明になると集中力が切れて「まあここは直感的に成り立つでしょ」と読み飛ばしてしまいます。
また数学者は例えば「\(x\) を一つとって固定する」ということをしますが、その正統性を説明できるのでしょうか？
私達は文字通り機械的にThmをcheckします。
それはいくつかのソフトで分担して行われます。代表的なものが Prover+ と Hyperion です。
Prover+はThmを「Prover9で処理しやすい形」にして送り、結果を受け取ります。
HyperionはThmからThmを作るということを行います。
会員募集
私たちは会員を募集しています。
システムの仕様詳細などの私たちの発明の核心的な部分は非公開です。共に議論しましょう！
「人間を考える作業から解放し、美しい世界へいざなう」という使命を共に背負いましょう。
代表：須田智彦[t@mshk1201.com]まで。
当会のAIエージェントは証明作成においても活躍してくれるハズです。
①web上のデータを大量に学習をしており、大学レベルの数学をこなす能力があります。
②当システムの仕様も学習しており、システムの道具を使いこなす能力もあります。
証明は ①数学知識を基に予想 → ②check を繰り返して作られます。
難しい定理では大量の試行錯誤は必要になりますが…兎にも角にも、AIによる証明を体験してみて！
AI時代には新しい数学観ができるハズです。
それは単に「作業が効率化する」というレベルにとどまらず、数学という学問の「定義」「価値」「人間の役割」そのものがアップデートされていくプロセスです。
「数学＝記号列を変換していくゲーム」「人間は結果を愉しむもの」という捉え方こそ、その「新しい数学観」の核を突いてるはずです。
大きく時代は変わろうとしています！