機械数学の歴史
数学の形式化はHilbertによって始められました。彼は1920年頃には完成していた一階言語を使おうとしました。「数学のほぼ全領域は一階言語で表現できる」とあるように、彼の目標は「原理的には」達成されています。
しかし、実際に数学を一階言語（あるいは、そのメタ言語としての自然言語）で表現しようとすると、すぐにうんざりする目に遭います。Burbakiの「数学原論」を読もうとしてもすぐに力つきます。
「一階言語のATP」も2010年頃には完成しています。proverを始めとして無料で使用できるATP softwareもあります。だから数学のATPも「原理的には」出来ていると言えます。四色問題の解決など一定の成果もあります。
しかし2020年頃の状況では、抽象数学において機械はほとんど役に立っていません。というかあまり研究もされていない感じです。
徒然なるままにちょっと哲学的な事を。
恐らく、意味は形式の上のレベルで処理されねばなりません。しかし、自然言語では一つの言葉に形式と意味を同時に持たせることができてしまいます…
見る対象の切り替えを迅速に行うことができますか？
空は青いし青くない(黒い)。
自己言及のパラドクスを避けるにはどうしたら良いですか？
この文には1が□個ある。
私たちのシステムは内部に何層もの階層を持ち、例えばRusselのパラドクスも自然に表現できます。
自然言語について
自然言語では大まかなニュアンスが伝われば良いようです。
最近、外国人による犯罪が増えています。
ってニュースはどう？
「最近」「外国人」「犯罪」どれをとっても思い浮かべるものは人次第なのでは？
そして、ただその事実のみならず「それは良くない事だ」という価値観まで伝え(あるいは植え付け)ようとしている？
私は自然言語を批判していますか？自然言語の性質を淡々と書いたつもりです。押し付ける価値観だって「こういう点では数学には適さない」くらいで。
もっと自然言語を擁護するとすれば、それは正確でない
私たちは意味を扱わないと言っても、意味はあると思っています。数学も芸術に昇華されるべきであって、鑑賞者の心を揺らさねばなりません。
余談ですが、「こういう時にはこうしましょう」と教える方が評価されるものです…本当に良い先生は「こういう時にはこういうやり方もある」と言います。
= とは？
世の中には沢山の = があります。前ページで
\(\log_{10}2=0.3\)
が出てきました。低レベルな入試では勝手にnealy equelの意味で = を使うことがあります。物理でもかも。昨日の自分と今日の自分は同じですか？
他の世界とは異質な = もあります。小学校では
\(3\div2=1\cdots1\)
でした。そしたら \(3\div2=4\div3\) ？
プログラミングの世界、例えば phpでも = は代入で
$x = 1;
は $x という箱に1を入れます(ニュアンスとしては)。そして返り値も1です。1 = $x; はエラーになります。同一かどうかの返り値が欲しければ == あるいは === を使います。
私たちのシステムはたくさんの = を使用します。
ところで低レベルな入試では勝手にnealy equelの意味で = を使うことがあります。物理でもかも。一つの世界の中では統一されるべきでしょう。そう言えば、小学校の算数では
\(3\div2 = 1\cdots1\)
でした。そしたら \(3\div2=4\div3\)？
定義にていて
テセウスの船
小学校では
\(3\div2=1\cdots1\)
でしたが、そしたら \(3\div2=4\div3\) ？
両方を採用することも(原理的には)可能です。
扱いやすさは機械にとってと人間にとってで大きく違うことが多いです。例えば \(1+1\) は機械内部では + 1 1 のハズ。
ものづくりの愉しみ
人類は多種多様な壮大なものを作ってきました。私たちもその一員となるべく、総合的に開発をしています。崇高な気概と遊び心を持った職人であらんと思っています。
ちょっとずつ丁寧に作ることも、難しい問題を一気に解決する閃きも必要です。シンプルで実用的、そして安心なソフトを作ろうと心がけていますが、新しい部分の作成にチャレンジするときは兎にも角にも作ってみるパワーが大事です。
機械は正確・忠実に命令を聞き実行します。指示をちょっと間違っただけで動かない奴にはイライラします。しかし、機械が「この定理は正しい」と返してきてくれた時は不思議な安堵を得ます。
ものづくりは面白いものです。
\( \displaystyle\frac{D}{A\class{reflect}{B}C} \)
何卒ご協力を
