主に高校数学を終えた方へ向けて。当会への勧誘も兼ねて。
証明
人類の行う行為の一つに「証明」があります。
それは「ある主張が正しいことを、誰が見ても納得できる理由のつながりで示すこと」です。
証明は紀元前6～3世紀のギリシャで始まりました。それ以前の古代エジプト・メソポタミアでも面積の公式はありましたが '正しい＝役に立つ' でした。ギリシャでは「なぜ必ず成り立つのか」を問う文化が生まれ、公理から論理で導くことが発明されたのです。
その後、中世ヨーロッパでは権威（神・古典）が重視されたり、16世紀以降では実験で検証される自然科学が証明から切り離されたり、時代によって証明は大きく変化しました。
現在では証明は多用な場面で見られ、それを避けて生きることは不可能になっています。小学校の算数で計算結果だけでなく計算式を書されるのは、証明行為の始まりと言えるかもしれません。身分証明書はなくしたら大変で面倒なことになります。通信では何らかの証明を機械が頻繁に行っています。
証明は分野ごとに異なる目的をもって行われています。仕事としてされる場合もあれば無意識のうちということもあるでしょう。誰が証明をし誰が判定するかや、基準・厳密さも色々です。裁判では「真である可能性が十分高い」程度でしょう。
数学の証明は疑いゼロだと言われています。しかし、ABC予想は2012年に望月教授により証明が発表され査読（何人かの権威ある数学者のお墨付き）もついたにも関わらず、懐疑的な数学者が多いようです。2025年、望月氏はLeanによる証明チェックを提唱しました。Leanは数学の新たな判定者になれるでしょうか？
私たちは、Leanより直感的に扱えて分かりやすいATPを作ろうとしています。数学の証明における確実さのレベルを一つ上に上げようとしています。正しさに振り回される定めからは逃れられなくても、せめて高いレベルでもがきませんか？
抽象数学
抽象数学というのはほとんどの人にとって馴染みがないでしょう。
しかしそれが「多くの人がイメージする（高校までの）数学とはかなり様相の異なったもの」ということは聞いたことがあるかもしれません。
大学数学でも最初の微積分と線形代数ではまだ計算が多いですが、抽象数学では論理が全面に出て「厳密性」が重要とされます。
\(8\div2(2+2)\) はアメリカだと\(1\)でイギリスだと\(16\)だそうです。議論をする時、まずその対象が明確になっていなくては困りますよね？
数列の極限は、高校数学では「無限に近づく値」とされますが、「無限」はまだしも「近づく」は感覚的な言葉で、不明瞭で使用に値しません。\(\epsilon, \delta\) などを使って厳密に定義することで、極限に関する定理の厳密な議論ができるようになるのです。
高校に入って場合分けで躓くように、大学に入って抽象化に躓くことがあります。
数学には所々に壁があって、それを乗り越えられないとその先に進めない、ということはあるかもしれません。
数学の歴史を見ると、19世紀に直感的な手法の限界が認識されたことが大きな転換点となったようです。
形式と意味
賢明なる読者は、高校数学の勉強で公式丸暗記では無く、きちんと意味を取る努力してきたハズです。
でも、意味を取ろうとするのは邪魔になることがあります。
\(\log_{10}2=0.3\Longrightarrow0=1\)
はどう読めば良いでしょうか？こういうのは難関大の入試なら出てくるでしょうが、次の問題はどうでしょうか。
\(x=0\) のとき \(1\div x=1\div x\) か？
言葉には形式と意味がありますが、人は普通は意味を取ろうとします。「幽霊は存在するか」という問いに「言葉として存在する」とは答えないようです。
自然言語では一つの言葉に形式と意味を同時に持たせることができてしまいます？
空は青いし青くない(黒い)。
形式主義の人は数学を形式的に扱います。
根源的な問にはしばしば沈黙します。例えば「集合とは何か」には答えません。Cantorを始め多くの人が頑張って説明しようとしてきましたが、「集合が満たすべき性質」があるだけ良いのです（公理的集合論の立場）。\(\sqrt2\) の定義は「\(2\) 乗して \(2\) になる正の数」で、初めのうちはよくわからないと感じるものでしょう。
数学の美と
数学の美を説く人がいます。深い理論や限りなく広がる世界に魅了された経験を持っているのでしょう。その途中では \(e^{i\pi}+1=0\) のような綺麗な式が待っていたのでしょう。
どんな分野でもその分野のすごさは部外者にはなかなか分からないものかもしれません。すぐには役に立たないもので人生を愉しめる事があるって事は言えそうです。
ピタゴラス教団が\(\sqrt2\)の無理性を発見したときには、どんな気分だったのでしょうか？
ところで、私自身は現状の数学をあまり美しく感じません。
数学者だって自然言語を使いますが、もうその曖昧さと言ったらひどいものです。数学の土台となる概念は集合ですが、ほとんどの数学者は「本当は…」などとごまかしています。
「\(x^2=1\) の解は \(x=\pm1\)」は \(\{x \mid x^2=1\}=\{1,-1\}\) とすべきですが、そんな表現は忌避されます。
機械にとっては、自然言語を使ったり厳密でなくする方が難しい…数列は「\(\mathbb{N}\) から \(\mathbb{R}\) への写像」と言う方が簡単なのですが。
形式主義は大学数学科でも忌避され、「数学では物事の構造を分かりその本質を理解することが求めらえる」と主張する人もいます。機械には到底できない事です。
私たちは抽象数学を機械に行わせようとしています。数学のめんどくさい部分は機械に任せ、ゆったりと数学を愉しみたいのです。
数学の奥深さに触れ感動することも、記号列が流れていくゲームを冷静に眺めるのも、共に味わうことはできるのでしょうか？
閃きを感じさせてくれる定理・細い線をつなぐような証明が冷めて見えても、機械からの数学世界の景色は人間の汚さを排除した眩いものになってくれるのでしょうか？
機械でこそ数学を芸術にできる、ってことはあるでしょうか？