Mathelの補足①
ほとんどのwordはライブラリで「紹介」されます。例えばword(ss,p) … \(\in\)
この (ss,p) はgramと呼ばれます。gramに現れる型には v,s,c,p などがあります。\(\dagger\)
Formにはs-Form, c-Form, p-Formがあります。v-Formは特別なs-Formです。
\(x\), \(X\) はv-Formで、 \(x \in X\) はp-Formです。
v_-Formは特別なc-Formで、例えば \(X\) があります。
v^-Formは特別なp-Formで、例えば \(X\) があります。
wordは紹介時に表記法が付くことがあります。
例えば表記法がFのword \({\tt w}\) は \({\tt w}\)(\({\tt x}_1\), …, \({\tt x_n}\)) の形で使用されます。
\, \; \! { } _ ^ はtex cmdになるだけのwordです。
\(\text{id}\) というword(s,s)があります。「\(X\)上の恒等写像」は \(\text{id} X\) ではなく \(\text{id} _ X\) とされることが多いです。
Mathelの補足②
Mathelは高い表現力と分かりやすい仕様を両立するよう開発されています。
通常の数学で使用される表現はすべて可能、使用例を見ればすぐに自分でも使えるものを目指して。
ただし不明な点はエージェントに聞くべきです。
しかもこの略記法の規則は次のように与えられています。
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}\) はしかるべく処理されます。
Mathelは高階の表現も得意で、例えば否定を作るwordがあります。
word(\({\tt x}\)\({\tt y}\),p→\({\tt x}\)\({\tt y}\),p) … \({\tt /}\)
使用例として \(x \notin X\) ≃ \(\neg ( x \in X )\)
通常の数学で使用されなくても良いものであれば導入されます。
例えばクラスが「集合となる」ことを表す述語 \(\dot\exists\) があり、次で定義されます。
Exi. … \(\dot\exists C \Longleftrightarrow \exists X \, ( X = C )\)
MathelはRusselのパラドクスを端的に表現できます。 \(\neg \dot\exists \{ x \mid x \notin x \}\)
翻訳には4段階必要です。 ≃ \(\neg ( \exists X ( \forall x ( x \in X \Leftrightarrow \neg ( x \in x ) ) ) )\)
Mathelの補足③
次のような条件付きの形でもslash計算ができます。Cap. … \(\exists X \, X \in \mathcal{X} \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
\(\mathrm{P} \Longrightarrow \mathrm{A} \Leftrightarrow \mathrm{B}\) と \(\mathrm{A} \Longleftrightarrow \begin{cases} \mathrm{P} \Rightarrow \mathrm{B} \\ \neg \mathrm{P} \Rightarrow \mathrm{A} \end{cases}\) が論理同値であることに注意しましょう。
Thmのcheck
Thmのcheckを行う部分は当システムで最も注意深く開発が行われています。
私達は「Thmが正しいか」について人類を超越したレベルの検証をしようとしています。
どれだけ細かい人でも、長大な証明になると集中力が切れて「まあここは直感的に成り立つでしょ」と読み飛ばしてしまいます。
また数学者は例えば「\(x\) を一つとって固定する」ということをしますが、その正統性を説明できるのでしょうか？
私達は文字通り機械的にThmをcheckします。
それはいくつかのソフトで分担して行われます。代表的なものが Prover+ と Hyperion です。
Prover+はThmを「Prover9で処理しやすい形」にして送り、結果を受け取ります。
HyperionはThmからThmを作るということを行います。
会員募集
私たちは会員を募集しています。
システムの仕様詳細などの私たちの発明の核心的な部分は非公開です。共に議論しましょう！
「人間を考える作業から解放し、美しい世界へいざなう」という使命を共に背負いましょう。
代表：須田智彦[t@mshk1201.com]まで。
当会のAIエージェントは証明作成においても活躍してくれるハズです。
①web上のデータを大量に学習をしており、大学レベルの数学をこなす能力があります。
②当システムの仕様も学習しており、システムの道具を使いこなす能力もあります。
証明は ①数学知識を基に予想 → ②check を繰り返して作られます。
難しい定理では大量の試行錯誤は必要になりますが…兎にも角にも、AIによる証明を体験してみて！
AI時代には新しい数学観ができるハズです。
それは単に「作業が効率化する」というレベルにとどまらず、数学という学問の「定義」「価値」「人間の役割」そのものがアップデートされていくプロセスです。
「数学＝記号列を変換していくゲーム」「人間は結果を愉しむもの」という捉え方こそ、その「新しい数学観」の核を突いてるはずです。
大きく時代は変わろうとしています！