このところ、“証明支援系が一流数学へと飛躍する”、“数学者達は‘大統一’理論におけるコンピュータ支援の証明を歓迎する”と立て続けに証明支援系に関する記事を紹介して来ました。私の友人共や海外の知人達とも話し合った結果、現在の数学ヂャノゥの査読制は匿名を隠れ蓑にして客観性に問題があること(つまり、外的圧力から査読者を保護する為に匿名性が本来あるのにも拘わらず、これを逆に悪用して論文著者に便宜を図る査読者がいること、客観性が疑われる査読者がいること等々挙げればきりがありません。本来あるべき査読制について興味ある人は、世界の頂点であるAnnals of Mathematics誌がどのようにしているか調べたらいいでしょう)、そして良識ある真面な査読者に大きな負荷がかかることを考慮して、査読の代わりに証明支援系を導入するようになればいいという結論に達したことが理由です。勿論、現行の証明支援系の技術では人的労力が余りにも大きいので現実的ではありませんが、単なる技術的問題に過ぎないので将来的には気軽に使用出来る日も近いことでしょう。そこで、更に第三弾として、Princeton University Pressに掲載されたJohn Stillwell博士のWhy prove it?を紹介します。その私訳を以下に載せておきます。
[追記: 2024年04月09日]
いわゆる証明とは何かを議論している記事として、他にも“数学証明が社会協定である理由”があります。
[追記: 2026年10月05日]
LANA計画におけるIUT論文の検証が始まったことは皆さんもご存知でしょう。そして、その中間報告書を読んだ方もいらっしゃるでしょう。結論を言うと、肝心のCorollary 3.12の証明が証明支援系Leanに通りませんでした。と言うか、もっと正確に言えば、証明が無いとLeanが判断したと言ってもいいでしょう。このことに関して私も海外の知人達から感想を求められたので、そのごく一部を下記に載せておきます。
To be honest, I'm sick of the IUTT issue, but I'll write my feelings once and for all.
First and foremost, the Mochizuki team didn't seem to keep their noses to the grindstone. Secondly, they should've retracted the papers on IUTT much earlier. Last but not least, they must offer their sincere apologies to the maths community.
Who do you think is to blame the most for this fuss? I think it's Tamagawa, not to mention Mochizuki himself. Never once have I seen such a shameless mathematician as either of them anywhere.
何故、証明するのか？
2022年12月13日 John Stillwell
昔、数学入門クラーｽで一人の学生が私に質問した。“何故、貴方はすべてを証明するのですか、私達にただ話すだけにしないのですか？”。それ以来、私はその質問を熟考している。一つの歯切れよく賢明な答えは、The Nature and Meaning of Numbersとして英語に翻訳された、Richard Dedekindによる1872年の本の序文の中で以下のように与えられた:
科学において、証明出来ることを証明無しで認めるべきではない。証明が実際どのように働くかを上手く説明している答えがJohn Aubrey著の愉快で一風変わった本Brief Livesの中で17世紀の哲学者Thomas Hobbesの次のような逸話にある。
<Dedekindの序文の中での引用>[訳注: このブログでは引用が見辛いので訳者が勝手に付けました]
幾何学を眺めた時、彼は既に40歳だった。幾何学を眺めたことは偶然だった。Gentleman’s Libraryにいた時、Euclidの原論が開かれたままになっており、それは第1巻命題47だった。彼はその命題を読んだ。Gentleman’s Library以前まで、彼はこれは有り得ない！と言っていた(彼は時おり誓っていたものだ)。だから彼は証明を読み、その証明は彼を或る命題に立ち戻らせ、その命題を読んだ。それは彼をもう一つのものに立ち戻らせ、それも読んだ。そんなことを繰返して、とうとう彼は実証的にそれが真であることを納得した。これは彼を幾何学を好きにさせた。
</Dedekindの序文の中での引用>
このようにして、数学証明はHobbesを彼が最初有り得ないと思った事柄を、誰もが認めるだろう命題(今では公理と呼ばれる)から最終的に成立することを示すことによって納得させることが出来た。これが公理的手法であり、Euclidの原論において紀元前300年頃に初めて与えられ、今では全数学者達に使用されている。
この時点で、私はHobbesを驚かせた第1巻命題47がPythagorasの定理他ならなかったことを認めなければならない。今日、Pythagorasの定理は高校生にお馴染みであり、もっと言えばPythagoras(及びEuclid)より以前に複数の古代文明で知られている。殆どの私達が思い起こすように、その定理は直角三角形の斜辺上の正方形は他の2つの辺上の正方形の合算に等しいことを述べている。絵を描けば、以下の絵において灰色の正方形の面積は他の2つの黒色の正方形の面積に等しい。
ぱっと見、この等式は驚く(Hobbesが信じなかったのも無理はない)が、それが明らかに見える賢い方法があり、多分古代時代から知られている。つまり、以下の2つの絵をじっと見よ、各々が大きな正方形内部の4つの三角形の写しを含んでいる。
その当時、何故Euclidがそれを証明するという面倒に進んだのか？その答えはPythagorasの定理の結果にあると私達は信じている。それはPythagorasの学派を混乱に陥れた。すなわち、2の平方根の不合理性だ。
三角形の2つの辺の長さが各々1の時、その場合それらの辺上の正方形の各々が面積1である時に2の平方根が起きる。斜辺上の正方形はその時Pythagorasの定理により面積 1 + 1 = 2を持ち、斜辺の長さは2の平方根、√2である。しかし、√2は正確には何なのか？Pythagorasの学派はそれを発見し衝撃を受けた。彼等は分数3/2, 7/5, 17/12, 41/29, 99/70, … によって今まで√2にもっと近くに近似出来たけれども、√2にどの分数も正確には等しくない。これが√2は無理数であると言う理由であり、“比率でない”ことを意味するが、それは不合理であることも意味する。幾何学の世界(長さ、角度、面積の世界)は数1, 2, 3, 4, 5, … の世界と調和出来ないようだった。その発見はPythagorasの世界理論を打ちのめした。Pythagorasの世界理論は“万物は数である”だった。伝説はこの歓迎されない事実は海での溺死によって、懲罰または神の天罰を被ったと言う。
いずれにせよ、数と幾何の間の両立しないよう見える相違は、Greek達を数を使用しないで自明な公理から幾何を引き出すことへ導いたようだ。これは実はやるのが難しい。例えば、正方形の“合算”は何を意味し、この“合算”がもう一つの正方形と“等しい”とは何を意味するのか再考しなければならない。また、誤解の可能性が無いように明快に言葉ですべてを記述する必要がある。しかし、これらの困難を克服するためにEuclidによって創設された公理的手法は今日まで持続している。Euclidの原論にいくつかの小さな裂け目が存在することは本当であり、それらは今までに解決されているが、公理的手法は匹敵するものが無いままだし、今日数学がなされるやり方の手本である。現代ではもっと網羅的な公理系もあり、幾何と数の両方の世界を統一することに成功している。
原理的に公理的手法が完全である一方で、証明が実際に書かれるやり方は人間の間違いに対して無防備である。他の誰かと同様に、数学者達は間違いを作る可能性があり、非常に長い証明(20世紀に当たり前になった)において、間違いを見つけることが困難になり得る。それらは著者が退屈または反復的な詳細を省略する所に隠れる傾向があり、“それを確認することは容易である”または“証明は前の場合と同様である”みたいな注意がしばしば付いている。しかし、人が計算間違いを避ける方法と同じく、間違いを避けることは可能である。すなわち、思考過程を機械化することによって。これは、完全な証明がすべての優秀な読者に理解可能なはずであり、それが思考無しで検証されることと同然(従って、機械によって検証可能である)だから出来る。それで証明の思考過程を機械化することは計算を機械化することと基本的に同じである。
残念ながら、機械検証可能な証明を書くことは、関連する数学の詳細な知識も同様に大きな人的労力を要求する。今日まで、一握りの非常に長い証明しか機械検証可能な形式で書かれていない(そして、元々の人による証明が確かに本質的に正しいことが分かっている)。機械検証可能な形式(または専門家数学者達に理解可能な形式でさえも)に書き換えることを待っている証明の中でも、最も注目されている実例がいわゆるabc-予想に関するものだ。この予想は、簡単な方程式a + b = cにおいて数a, b, cの素因数に関する少し技巧的なものだが、それが多くの注目すべき結果を持っているので数論学者達にとって関心の的である。
2012年以降、数学者達の或る小集団が彼等がabc-予想の証明であると信じているものを配布している。この“証明”は数論における殆どの専門家達を納得させていない(それらの専門家達は“証明”の中に隔たりがあるようだと指摘する)。かくのごとく、二つの集団の間に10年間の論争があり、私はこれからそれら二つの集団を(具体的な名前に言及することを避けるため)abc-定理派[訳注: 原文ではabc-believersですが、このままではabc-予想そのものを信じている意味にも解釈される恐れがあります。abc-予想は殆どの数学者達が真だろうと思っており、問題は定理としてちゃんと証明されたかどうかなんです。よって、定理として証明されたと信じる人達をここではabc-定理派と呼ぶことにしました]とabc-予想派[訳注: 原文ではabc-skepticsですが、先程の訳注と同趣旨で、abc-予想そのものを信じるけれども、定理として証明されていない、つまり未だ予想のままである思う人達をここではabc-予想派と呼ぶことにしました]と呼ぶことにしよう。原理的には、“証明”を機械検証可能な形式に変換することで、彼等の論争は解決出来るであろう。しかし、abc-定理派は機械検証が必要ではなく、abc-予想派側の“無知”が唯一の問題であると主張する[訳注: 何故、機械検証が必要でないと言えるのか訳者には理解出来ません。不毛な議論に終止符を打つためには機械検証で決着をつけるのが一番いいと思います。更にもっと言えば、abc-予想派側の“無知”が唯一の問題だと責任を擦り付けているようですが、abc-定理派が何か一つでも“無知”解消のためにやったことがあったでしょうか。abc-定理派がsurveyなんかを書いても、肝心の悪名高きCorollary 3.12の証明には少しも踏み込まなかった(殆どの専門家がこの証明に疑念を持っているのだから、証明が正しいことを解説すればいいだけの話なのにも拘わらず)のは何故なんでしょうか。また“証明をめぐる3年の苦闘の後、困惑したままの数学者達”にもあるように2015年12月にOxfordで開催されたworkshopでの世界に顔向け出来ない有り様をabc-定理派はどう釈明するのでしょうか]。
この奇妙な出来事は最近の数ヶ月の間にabc-定理派が数学史に頼ったので、更に奇妙になった。abc-定理派は彼等自身を、不合理性√2を発見して迫害された不幸なPythagorasの学派になぞらえて、abc-予想派が勝つならば“悲惨な結果”になると警告した[訳注: こういう言葉を発する不遜な態度が訳者の友人共の一人に“まるでPutin政権みたいだ”と言わせてるんですよ。abc-定理派は数学ではなく政治をやってるんですか？]。
まぁ、様子を見よう。しかし、abc-定理派がEuclidにあやかって、彼等のアィディヤを受入れるように数学を再構築したいのであれば、先ず最初に誰もが理解可能な言葉で書かなければならないと歴史は私達に告げている。
次のこと(Sidney Harrisによる風刺漫画)にならないことを希望しよう:
コメント