形式と意味
数学を形式的に扱う際は、意味には触れません。
例えば「集合とは何か」には答えません。Cantorを始め多くの人が頑張って説明しようとしてきましたが、「集合が満たすべき性質」があるだけ良いのです。\(\sqrt2\) の定義は「\(2\) 乗して \(2\) になる正の数」です。
意味を取ろうとするのは邪魔になることすらあります。
\(\log_{10}2=0.3\Longrightarrow0=1\)
はどう読めば良いでしょうか？
記述は機械に処理できることが必要十分です。自然言語を使ったり意味を訴えることはできません。
「\(x^2=1\) の解は \(x=\pm1\)」は許容されません。\(\{x \mid x^2=1\}=\{1,-1\}\) としましょう。
Perspektivismus
人間は同時に二つの視点を持つことができません。その事実を知り、必要であれば切り替えを迅速に行うことが肝要です。次の文は？
空は青いし青くない(黒い)。
意味は形式の上のレベルで処理されねばなりません。それを誤ると例えば自己言及のパラドクスが起こります。
この文には1が□個ある。
私たちの言語は内部に階層を持ち、Russelのパラドクスも自然に表現できます。
数学の形式化
数学の形式化はHilbertによって始められました。彼は1920年頃には完成していた一階言語を使おうとしました。「数学のほぼ全領域は一階言語で表現できる」とあるように、彼の目標は「原理的には」達成されています。しかし、実際に数学を一階言語で表現しようとすると、すぐにうんざりする目に遭います。
形式化により冗長・雑多になるのを避け簡潔に済ます方法を模索することは、地味かもしれませんが創造的でやりがいがあります。数学の新しい内容を作のではなく新しい表記を与えることが、より大きな世界への扉を開くはずです。
数学の機械化
「一階言語のATP」も2010年頃には完成しています。proverを始めとして無料で使用できるATP softwareもあります。だから数学のATPも「原理的には」出来ていると言えます。四色問題の解決など一定の成果もあります。
しかし2020年頃の状況では、抽象数学において機械はほとんど役に立っていません。機械は、単純な計算では人間を凌駕しても、少し高度なことをやらさせると計算量が爆発してしまいます。
機械は意味を理解しないし人間の直観に当たるものを持ちませんが、忠実に命令を聞き何より正確です。その良い点を数学に生かすことはできるはずです。
方針・目標
私たちは洗練された道具で数学を形式化・機械化します。
機械での計算はいろいろなsoftwareを連動させて行わせます。その最終部分はproverに任せます。mathmaticaなどの計算ソフトや人工知能も、将来的には取り込みたいです。
数学のめんどくさい部分は機械に任せ、その美しさに手軽に触れられるようにすることが第一コンセプトです。システムはできる限りシンプルにし、人間が容易に扱えるようにすべきです。形式的な列を眺めつつ、意味を汲み取ることで楽しみましょう。
色々なことができるようにしたいですが、ま、迷走しきりです。何を作りたいのか、は頻繁に見失ったり新しく出てきたりします。始まりは満足いく形で数学の結果をまとめておきたいだけだったのです。
数学者の相棒と言えるくらいのレベルになって欲しいです。証明のチェックって大変らしいので補助できるように。
そしたらABC予想の懸賞金を取りに行きます。定義が多くこまごましたものは、機械がやるべきです。
もっと発展して、数学者の仕事を奪って、大きな世界への扉を開いてくれれば？人間には発見出来ないような定理や証明を見たいです…
いずれAIが数学をやるようになったとき、新しい世界では新しい芸術があるでしょうか？
\( \displaystyle\frac{D}{A\class{reflect}{B}C} \)