かなり前に紹介した“証明支援系が一流数学へと飛躍する” の前置きの中で御登場願った欧州某国の知人(非英語圏の方です)が来日を終えて無事に帰国したことを知らせてくれたので、その返信として月並みですが、How did you like Japan?と書き送ったところ、旅行記かと思う程詳細な感想を書き寄越してくれました。その最後のごく一部分をそのまま書けば以下の通りです。
Lastly, I was surprised that most Japanese people didn't understand English. I couldn't have enjoyed myself in Japan without you. I'm indebted to your help. If you're ever here, please feel free to contact me anytime.
I'm looking forward to seeing you again.
もっと補足すると、その欧州某国の知人(何回も言うようですが、非英語圏の方です)は日本で私と離れて行動する時に(私も24時間ずっと傍らにいることが不可能なので)、事ある毎に翻訳機等を日本人から顔に突き付けられるので、白けてI'm ok, thank you.と言って立ち去るしかなかったと言ってました。これに対する私の返信が以下です。
You aren't alone. Many other foreigners who've been to Japan often ask me why most Japanese people don't even understand English despite having had an English education for at least six years (nearly ten years, including the time spent in university or college). Only can I answer that they're gormless and haven't even studied other subjects seriously, much less English, in school. It can’t be helped. What do you say to that?
次いでながら、米国の知人から数学とは別の話題、すなわち最近のニューズで話題になっている大谷翔平選手の事件に関して、何故それ程までに水原一平氏に頼ったのか疑問だと書いて来たので、以下を率直に書いて送りました。
Of course, I'm not in a position to comment on this incident; I'm, however, grateful that the incident has chilled the enthusiasm of the Japanese for Shohei Ohtani a little. I hope that most Japanese people will open their eyes to his nature and that they'll have an eye for a person. Who can vouch that he doesn't in the least relate to Ippei Mizuhara's gambling? He's at best only a baseball player and might be anything but a person of integrity. While he's lived in the US for at least six years, it's odd enough that he doesn't speak English much. That shows he hasn't yet been independent of others, except for playing baseball. If he doesn't realise it, it must be said he's nothing but a naked king. I hope he doesn't let so many people down.
要は私の海外知人達から見れば、日本の平均知的水準を考慮すると本当に先進国なのか疑問だということですね。
さて今回紹介する記事はQuanta誌に掲載されたAnrewd Granville博士のWhy Mathematical Proof Is a Social Compactです。これを選んだ理由は簡単で、相変わらず日本の某数学者の小集団が世界のコミュニティを蔑ろにして好き勝手なことをほざいているからです。その小集団のみならず、彼等を取り巻く馬鹿fansも付和雷同するのを見て呆れました。ともかくも、その私訳を以下に載せておきます。
[追記: 2024年04月08日]
この私訳を載せた途端に、例の某数学者の小集団がまたまた変なことをしでかしたので、私も海外知人達から意見を求められ、以下を素っ気なく書き送りました。
It's no use advising Mochizuki's team that it should usually be incumbent on authors to explain their papers to others so they can understand because, as is often the case with Mochizuki's team, this kind of advice deliberately goes in one ear and out the other. Thus, it was virtually they who parted company with the maths community. They would stop at nothing in Japan to save their face. For example, they've long since even gone so far as to hype their achievements only inside Japan using foolish Japanese media, institutes and more foolish Japanese fans. They seem very good at only self-promotion. For the record, the ABC conjecture is still open as long as the validity of Mochizuki's proof of Corollary 3.12 is unexplainable and almost all experts, except Mochizuki's team, question its validity. With all these situations, does anyone want such an almost self-congratulatory prize? If that's the case, it must be said the person is shameless. Mochizuki's team has lowered themselves towards a much lower level than expected. I question if they know what they're doing. All we have to do now is to wait and see. We had better leave them the way they are. You have only to ridicule their big fuss.
[追記: 2024年04月10日]
いわゆる証明とは何かを議論している記事として、他にも“何故、証明するのか？”があります。
[追記: 2024年04月20日]
望月新一博士の最新のreportを読んだ人も多いかと思います。数学的議論を別にして、あの悲劇の9/11をわざわざ持出して、Kirti Joshi博士の論文の定理の番号付けがどうたらこうたら云々と難詰しているのを読んで非常に嫌悪感を抱いたのは私のみならず、私の友人共や海外知人達も同様でした。いや、私は恐怖すら覚えました。私の海外知人達の間では数学的議論に全く関係の無いことでJoshi博士を甚振るのは余りにもおかしいと正式抗議のために署名運動等を始めようかと言い出す方もいらっしゃいます。それに対する意見を求められたので、差し障りの無い範囲で私の意見のごく一部を以下に載せておきます。
Mochizuki insulted Kirti Joshi apart from mathematical arguments in his new report. It's obvious harassment or disdain towards her to all appearances and a violation of human rights. You might want to challenge Mochizuki on that report through the IMU and exclude Mochizuki from the maths community if he refuses to apologise. You should, however, bear in mind that the incumbent president of the IMU is unluckily Japanese and worse yet an ex-professor of that infamous RIMS, so the insiders of the IMU might stop your movement in a cowardly manner at a certain stage. The best way is for the victim, Kirti Joshi, to accuse Mochizuki of violating human rights as soon as possible through the IMU. It may be, however, difficult for her to do so for now, considering her conditions. Much to our surprise, Mochizuki almost always insults others' intelligence although few think much of him. Does he perhaps want to get disliked deliberately by the maths community except Japan? If that's the case, I can't help but say how singular a country Japan is. If you leave Mochizuki the way he is, you have no choice but to grin and bear his insults. Incidentally, an acquaintance abroad says Mochizuki's papers on IUTT have long since been white elephants and that they aren't worth your attention as long as the validity of Mochizuki's proof of Corollary 3.12 is unexplainable. So you don't need to have any reservations about Mochizuki. Few are troubled without IUTT. I'd rather sign the signature list if you can promote the movement than merely stand with you. I couldn't agree more with you.
Be that as it may, I'm very disappointed that Mochizuki's companions didn't tell him where to get off. You'll soon notice there's no decent person around him.
数学証明が社会協定である理由
2023年08月31日 Jordana Cepelewicz
2012年、数学者 望月新一はabc予想を解決したと主張した。abc予想は加法と乗法の間の関係に関する数論における主要な未解決問題だ。ただ一つだけ問題があった。すなわち、500ペィヂ以上の長さの彼の証明が全く不可解なことだった。殆どすべての数学者達にとって理解不能な新しい定義、数学的表記法、理論の混沌に基づいていた。数年後、二人の数学者達が証明の大部分をもっと馴染み深い表現に翻訳した時、彼等はその証明の中に彼等の一人が言う所の“深刻で修正不能な隔たり”を指摘したが、望月は彼等が論文を単に理解し損なっているとして彼等の議論を却下した。
その出来事は根本的問題を引き起こしている。すなわち、数学証明とは何であるか？私達はそれを外的真実の新たな発覚であると考えがちであるが、おそらく社会的構築物として考えた方がいいだろう。
the University of Montrealの数学者Anrewd Granvilleはそれについて最近ずっと考えて来ている。彼が書いた著作のいくつかについて哲学者が連絡して来た後に、“どのように私達は真実に到達するのか考えるようになった。いったんその扉を開けると、それが広大な議題であることが分かる”と彼は言った。
Granvilleは若年の時から数論に親しんだが、数学研究におけるカリヤを考えなかった(そんなことが存在することを知らなかったので)。“私の父は14歳で学校を卒業し、母は15または16歳で卒業した。彼等は倫敦で当時の労働者階級の地域で生まれたので、大学が可能であるとは思わなかった。私達は分からなかった”と彼は言った。
彼は数学を勉強したケィンブリヂ大学を卒業した後に、Martin Amisの小説The Rachel Papersを映画台本に翻案することを始めた。その計画のための作業と資金援助を探している一方で、彼は事務仕事を避けたかった(彼は高校と大学の間の隔年の期間に保険会社で働いていた)。“だから私は学校を卒業しに行った”と彼は言った。その映画は離陸することは無かったが(小説は後で別個に映画になった)、Granvilleは数学で修士を得て、博士課程を完了するために加奈陀へ移った。彼は決して後を振り返らなかった。“本当に冒険だった。私は多くを望まなかったし、本当にPh.Dが何たるか知らなかった”と彼は言った。
それ以降数十年の間に、彼は主として数論に関する175本以上の著者である。また彼は大衆のための数学に関する著作で有名になっている。例えば、2019年に彼は年上の姉である脚本家のJenniferと素数及び関連概念に関する長編漫画を共著した。先月、“どのように私達は真実に到達するか”に関する彼の論文の一つがthe Annals of Mathematics and Philosophyにおいて発表(PDF)された。そして、他の数学者達、計算機科学者達、哲学者達と共に彼は来年のBulletin of the American Mathematical Societyに、どのように計算機が数学を変えるかも知れないかに関する一連の論文を発表することを計画している。
Quantaは数学証明の性質(証明が実際にどのように証明に関するお馴染みの誤解に働くかから、人工知能の時代に証明を書くことがどのように進化するかまで)についてGranvilleと話しをした。そのインタヴューは明晰性のために編集され圧縮されている。
最近貴方は数学証明の性質に関する論文を発表しました。どうしてこれを書くことが重要であると決心したのですか？
数学者達がどのように研究を行うかは一般的に大衆向けミーディヤにおいて上手く描かれてない。人々は数学を純粋な探究、純粋な思考のみで真実に辿り着くものとして考える傾向にある。数学にとって推測が肝要であり、その推測は屡々間違っている。それは実験的過程である。私達は段階ごとに学習する。
例えば、1859年の論文にRiemann仮説が初めて登場した時に、それは魔術だった。すなわち、やぶから棒に魔術的予想がここにあります、だ。70年間、人々は純粋思考のみで偉大なる思考者が何を出来るのかを語った。そしてそれから、数学者 Carl SiegelがGöttingenのアーカイヴｽﾞの中にRiemannのメモ書きを見つけた。Riemannは実の所Riemannゼィタ函数の零点の計算を何ペィヂもやっていた。Siegelの有名な言葉は“純粋思考のみの話はこれでお終い”だった。
それで人々(特に何人かの哲学者達と歴史家達)が数学について書くやり方に不安がある。彼等は自分達が或る純粋奇跡の生物、科学の或るユーニコーンだと思っているらしい。だが、典型的に私達はそうではない。純粋思考のみは滅多にない。
数学者達がしていることをどのように特徴づけますか？
数学文化にとって証明が肝要だ。そこらに座って考え、私達がやっていることの95％が証明だ。私達が得る理解の多くが、証明との苦闘と問題と格闘する時に来る問題の解釈から来る。
私達は数学的議論を証明として考えがちです。論理的段階の連続を通して、与えられた命題が真であることを実証します。しかし、貴方はこれを純粋で客観的な真実と誤解すべきではないと書いています。それは何を意味するのでしょうか？
証明の主要点は読者に言明の真実性を納得させることだ。それは検証が鍵であることを意味する。私達が数学の中で持っている最善の検証システムは、多くの人達が異なる観点から証明を見ることであり、それらの人達が知っていて信じている状況において、それは上手く行く。或る意味で、それが本当だとは言えない。多くの人達が異なる観点から試しているのだから正しいと思っているとは言える。証明はこれらのコミュニティの標準によって了承される。
その時に、この客観性という概念がある。すなわち、主張されていることが正しいという確信、究極的に真実であるという感覚だ。だが、客観的であることをどのように知ることが出来るのだろうか？既に命題を作ってしまっている状況から自分を連れ出すこと、つまり社会によって既に定まっている理論的枠組みの外側の観点を持つことは困難だ。これは科学的アィディヤに対して他の物事と同様に真実だ。
数学において、何が興味深い又は重要なのかを問うことも出来る。しかし、これも明らかに主観的だ。Shakespeareが何故いい作家なのか私達は考えるか？Shakespeareは彼の生きた時代においては今日と違って人気が無かった。何が興味深く、何が重要かの周辺には明らかに社会協定がある。そして、それは現行の理論的枠組みに依存する。
数学において理論的枠組みは何に似ているのでしょうか？
理論的枠組みの変換の最も有名な例の一つが微積分だ。微積分が発明された時、零に近づく何かを零に近づく別の何かで割ることを伴った。つまり、零を零で割ることに繋がるが、それは何の意味も持たない。最初NewtonとLeibnizは無限小と呼ばれるオブジェクッを思いついた。それが彼等の方程式を働かせたが、今日の標準により無限小は賢明でも厳密でもなかった。
今や私達はε-δ体系を持っており、それは19世紀の終わりに導入された。この現代的定式化はこれらの概念を驚くほど明晰に正しくするので、古い定式化を見る時、彼等は何を考えていたのかと思う。しかし、当時それが微積分出来る唯一の方法だと考えられた。LeibnizとNewtonに公平に言えば、彼等もおそらく現代的方法を愛したであろう。彼等の時代の理論的枠組みのために彼等は現代的方法をやることを考えなかった。だから、そこに辿り着くために恐ろしい程長い時間を要した。
問題は、そのように行動している時を知らないことだ。私達がいる社会の中で私達は罠にかかる。私達が作っている何の思い込みかを言う外側の観点を私達は持っていない。数学における危険の一つは、何かを貴方の使用している言語内で容易に記述又は議論出来ないから、それを重要でないと貴方が考える可能性があることだ。それは貴方が正しいことを意味しない。
私はDescartesによる次の引用句が本当に好きだ。そこでは本質的に“私は三角形について知っておくべきことはすべて知っていると思うが、誰が私がそうだと言うのか？未来の誰かが革新的な観点を思いつき、三角形を考えることについてずっと良い方法に繋がるかも知れないことを私は意味している”と言っている。そして私は彼が正しいと思う。数学においてそれを見る。
論文で貴方が書いたように、証明は社会協定、つまり著者と数学コミュニティの間の一種の相互合意だと考えられます。これが機能しない極端な実例、abc予想に関する望月が主張する証明を私達は既に見ています。
望月は社会協定が機能するやり方でゲィムをしたくなかったから極端だ。彼はこの選択を目立たないようにしている。実に新しく難解なアィディヤを伴う大発見をする時、それらのアィディヤを出来る限り近づき易く説明することにより他の人達を含めるように努めることは発見者の義務だと私は思う。そして彼は言ってみれば、自分が書いた通りに貴方が読みたくなければ、それは自分の問題ではないと言っている。彼は自分がしたいようにゲィムをする権利を持つ。だが、それはコミュニティと何の関係も無い。私達が進歩する有様とも何の関係も無い。
証明が社会背景の中にあるならば、証明は時間が経つに連れてどのように変化して行くでしょうか？
それすべてAristotleで始まる。彼は或る種の推論システムが存在する必要があると言った。つまり、良く知っていて確信している事柄に基づいて新しい事柄を証明出来て、或る“原始命題”又は公理に遡る。
だから、その時の疑問はこうだ。貴方が真だと知っている基本事項とは何なのか？非常に長い間、人々は言ってみれば、線は線であり、円は円であると言った。簡単で明晰な少数の事柄が存在し、それらは開始するための仮定でなければならない。
その観点は永遠に続いている。それは現在付近でも大部分続いている。だが、発展したEuclidean公理システム、すなわち“線は線である”は問題を抱えた。集合の概念に基づいてBertrand Russellによって発見された逆説があった。更に言えば、“この命題は偽です”(それが真なら、その時は偽であり、それが偽なら、その時は真である)のような問題のある命題を作りながら数学言語で言葉遊びが出来た。それは公理システムに問題があることを示した。
だからRussellとAlfred Whiteheadは、これらの問題すべてを避けられて数学をする新しいシステムを作ろうと努めた。しかし、それは馬鹿々々しい程複雑で、これらが正しい開始点だと信じることは困難だった。誰もそれを快適だと思わなかった。2 + 2 = 4を証明するようなものでも開始点から膨大なスペィスを要した。そんなシステムの問題の核心は何なのか？
その時David Hilbertがやって来て、次のような素晴らしいアィディヤを持った。すなわち、開始するにあたって何が正しい事柄かを話すべきではないだろう。代わりに、機能する事柄(開始点が簡潔で理路整然としており矛盾が無いこと)を探究することに価値がある。お互いが矛盾する公理から二つ事柄を推論出来ず、選ばれた公理に基づいて数学の大部分を記述出来るべきである。しかし、それらが何であるか先天的に言うべきでない。
これも数学における客観的真実に関する先の私達の議論に合致しているように思います。ですから、20世紀の折り返し時点で、数学者達は複数の公理システムが存在するかも知れないことを気付いていた。つまり、公理の集まりを与えられている事柄を普遍的又は自明的真実として考えるべきでないと？
正しい。そしてHilbertは抽象的理由のためにこれを始めたのではなかったと私は言わなければならない。彼は幾何学の異なる概念、つまり非Euclidean幾何学に非常に関心があった。非Euclidean幾何学は大変論争が多かった。当時の人達は言ってみれば、箱の隅周辺に行く線の定義を貴方が与えるならば、一体何故私が貴方に耳を貸すべきなのか？だった。そしてHilbertは定義を理路整然として無矛盾にすれば耳を貸すはずであると言った。何故なら、これが私達が理解する必要がある、もう一つの幾何学かも知れないからだ。そして、観点における変革、すなわち任意の公理システムを認めることは幾何学に適用されただけではなかった。数学のすべてに適用された。
しかし、もちろん幾つかの事柄は他よりも役立つ。だから、私達の殆どが同じ10の公理、ZFCと呼ばれるシステムと共に研究する。
それから何が推論出来て何が出来ないのかという疑問に繋がる。連続体仮説のような命題が存在するが、それはZFCを使って証明出来ない。第11番目の公理が存在するはずだ。貴方が貴方の公理システムを選べるのだから、いづれかの方法で解決出来る。それは非常に素晴らしい。私達はこの種の複数性と共に続いている。何が正しく、何が間違っているのかはっきりしない。Kurt Gödelによれば、私達はまだ好みに基づいて選択する必要があり、良い好みを持っていることを希望する。私達は意味のあることをしなければならない。そして私達はしている。
Gödelと言えば、彼はここでも大きな役割をしています。
数学を議論するためには、言語そして言語の中で従うべき規則の集まりを必要とする。1930年代において、どのように言語を選ぼうが、その言語の中に真であるが、始まりの公理から証明出来ない命題が必ず存在することをGödelは証明した。実を言うと、実際はそれよりももっと複雑なものであるが、それでも、貴方はこの哲学的板挟みをすぐに持っている。すなわち、貴方が正当化出来ないなら真の命題とは何なのか？馬鹿げている。
だから大きな困った事態がある。出来ることの中に私達は制限されている。
職業数学者達は大方これを無視している。何が実現可能かに焦点を絞っている。Peter Sarnakが好んで言うように“私達は労働者だ”。私達が出来ることを続け証明しようと頑張っている。
今や、コンピュータのみならずAIさえも使用して、どのように証明の概念が変わりつつありますか？
私達は既に異なる場所、コンピュータが突飛な事柄を出来る場所に移っている。今や、おぉ私達はこのコンピュータを持っており、人が出来ないことを出来ると人々が言う。だが、そうなのか？人々が出来ないことを実際に出来るのか？1950年代に遡れば、Alan Turingはコンピュータは人間が出来ることを(ただ単に早く)出来るように設計されていると言った。多くは変わっていない。
数十年間、数学者達はコンピュータを使い続けている。例えば、彼等の理解への導きを助けられる計算を行うために。AIが出来る新しいことは私達が真だと信じている事柄の検証だ。いくつかの素晴らしい発展は証明検証と共に発生している。Lean[証明支援系]のように、証明支援系は数学者達が多くの証明の検証をすることを可能にする一方で、著者達が自分達の成果をより良く理解することを助けている。数学者達は検証のため彼等のアィディヤを簡潔な段階に分解してLeanに供給しなければならないからだ。
だが、これが絶対確実なのか？ただ単にLeanが正しい証明と言うから証明が証明なのか？いくつかの意味で、それは証明をLeanへの入力に変換する人達と同等に良いことだ。私達がどのように伝統的数学をするのかに非常に似ているように思われる。だからLeanのような何かが多くの間違いを作るだろうと信じると私は言っているのではない。人類のよって為されるものよりも安全だという確信を持てないだけだ。
残念ながら私はコンピュータの役割について大いに疑問を持っている。コンピュータが事柄を正しくするための非常に価値ある道具にはなり得る。特に、初見で分析が容易でない新しい定義に支えられている数学を検証することに対しては。私達の兵器庫の中に新しい観点、新しい道具、新しい技術を持つことは役立つということの議論が無い。しかし、私が避けていることは正しい定理を生産する完全な論理機械を今や持とうとしているという考え方だ。
コンピュータを用いて事柄が正しいと確信出来ないことを認めるべきだ。私達の未来は科学の歴史を通じて私達が頼って来ているコミュニティの感覚に頼らなければならない。すなわち、事柄を互いにぶつけて反応を見ること、完全に異なる観点から同じ事柄を見ている人達と話すこと、等々だ。
けれど、これらの技術が高度になるに連れて、将来これがどこに行くと考えますか？
多分、証明を拵えるにあたっての支援をするだろう。5年以内かも知れないが、私はChatGPTのようなAIモドゥに“私はこれをどこかで見たことがあると確信します。それを調査してくれますか？”と話しているだろう。そしてAIモドゥはそれは正しいという同じ言明を返すだろう。
そしてそれから、それが一旦大変良ければ更に段階を進めて“私はこれのやり方を分かりませんが、これと同じような事柄をやってしまっている人がいますか？”を言えるであろう。多分結局、AIモドゥはどこか他で使用されて来ている道具を用いるための文献を熟練した方法で見つけ出すことになろう。つまり、数学者が予見しないだろうやり方で。
しかしながら、どのようにChatGPTが私達を追い抜くように証明をする或るレベルを超えるのか私は理解出来ない。ChatGPTや他のプロゥグラァム学習機械は思考しない。それらは多くの実例に基づいて連想される言葉を使用している。だから、それらが訓練用ディタを超越するだろうことはありそうにもないように思える。だが、仮にそれが起こるとすると、数学者達は何をするのだろう？私達がやることの大部分が証明だ。私達から証明を取上げるなら、私達は誰になるのか分からない。
それでも、コンピュータを支援系とする場合を考える時、人類の努力から学んで来ている全教訓を考慮する必要がある。すなわち、異なる言語を使用すること、共同研究すること、異なる観点を抱えることの重要性だ。どのように異なるコミュニティが共同研究し、証明を理解するのかの中に厳密性、健全性が存在する。数学の中にコンピュータを支援系として持とうとするなら、同様なやり方でそれを豊かにする必要がある。
コメント