taro-nishinoの日記

 このところ、“ 証明支援系が一流数学へと飛躍する ”、“ 数学者達は‘大統一’理論におけるコンピュータ支援の証明を歓迎する ”と立て続けに証明支援系に関する記事を紹介して来ました。私の友人共や海外の知人達とも話し合った結果、現在の数学ヂャノゥの査読制は匿名を隠れ蓑にして客観性に問題があること(つまり、外的圧力から査読者を保護する為に匿名性が本来あるのにも拘わらず、これを逆に悪用して論文著者に便宜を図る査読者がいること、客観性が疑われる査読者がいること等々挙げればきりがありません。本来あるべき査読制について興味ある人は、世界の頂点である 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 did...

ペータ・ショルツェ博士が証明に対して実に真摯なことは、前に紹介した“ 証明支援系が一流数学へと飛躍する ”を読んだ人なら良く分かっただろうと思います。ブルバキの言葉を引用するまでも無く、古代Greeceの昔から数学とは即ち証明なんです。自らの証明に何らかの違和感を持つ場合は勿論のこと、他者から証明に疑念を持たれること自体が数学論文としては失格なんです。証明をないがしろにすることは数学をないがしろにすることと同義です。証明が自明であるという陳述だらけの論文をどこかで見たことがありますが、数学への冒涜以外の何ものでもありません。そういうものを好きな人は哲学又は宗教学をやればいいのではないでしょうか。 “ 証明支援系が一流数学へと飛躍する ”はどちらかと言えば、ショルツェ博士に焦点を当てた記事でした。もう少し他の関係者にも触れた記事として Nature 誌に掲載された Mathematicians welcome computer-assisted proof in ‘grand unification’ theory があります。私はこちらの方がいわゆる群像劇という意味合いで面白かったように思います。その記事の私訳を以下に載せておきます。 数学者達は‘大統一’理論におけるコンピュータ支援の証明を歓迎する 証明支援プロゥグラァムは抽象的な概念を処理して、数学でのソフッウェアのより大きな役割を明らかにしている。 2021年06月18日 Davide Castelvecchi ペータ・ショルツェは現代数学の大部分を再構築したいと思い、その基礎から始めている。彼の探究の心臓部に対する証明が正しいことを思わぬ情報源から受けている。すなわち、コンピュータである。 殆どの数学者達は彼等の専門職の創造面にいつでもすぐにコンピュータが取って代わるだろうことに懐疑的であるけれども、何人かの数学者達は彼等の研究において科学技術が益々重要な役割を持つことを認めている。そして、この特別な偉業が証明支援系を認めることへの転換点となるだろう。 数論学者ショルツェは独逸のボン大学(そこに彼は本拠を置いている)での一連の講義において大掛かりな計画(コゥペンヘィゲン大学のDustin Clausenとの共同研究)を述べた。その二人の研究者達はそれをcondensed mathematics[訳注:...

2022年01月13日にグロタンディーク氏の Récoltes et Semailles (以降 R&S と略記します)がやっと仏蘭西でGallimard社から出版されたことは皆さんも御存知でしょう。これはグロタンディーク氏がお亡くなりになり、それと前後して同時代の有力数学者等の関係者も故人となっているので遅かれ早かれ出版されるであろうことは誰もが予想していたことでした。しかし、文芸出版の老舗であるGallimard社から出版されることは少なくとも私には予想外でした。Gallimard社は R&S をノンフィクシュンではなく、あくまで創作物と見なしているのかも知れません。だから、ひょっとして訴訟沙汰になるかも知れぬ作品の出版を決断したのでしょう。 そうは言っても、関係者全員が故人になったわけではなく、例えばグロタンディーク氏が執拗に攻撃した弟子筋ではドリーニュ博士等がご健在だし、気の毒にも全く的外れの攻撃対象になった日本の柏原正樹博士もいらっしゃるし、よく出版を決断出来たなぁと感心してたら、仏蘭西の知人がそれらの人達はグロタンディーク氏よりも年下だけど遥かに大人だよと書いて来ました。勿論Gallimard社はプロの出版社ですから、用意周到に何年も前から関係者各位に根回しをしたことは間違い無いでしょうが、確かに上記の人達が大人でなければ成立しません。 さて、今回紹介する記事は Inference に掲載されたPierre Schapira博士の A Truncated Manuscript です。これは出版された R&S を書評対象とするリヴューです。Schapira博士と言えば、佐藤幹夫博士を頭とする、いわゆる佐藤学派の擁護者としても有名であり、柏原正樹博士との共著 Sheaves on Manifolds を読んだ人も多いことでしょう。  Schapira博士は出版された R&S にはグロタンディーク氏の追記と脚注の最新のものが含まれていないことを疑問視しています。仏蘭西の知人ともe-mailで議論した結果、私はそれは止むを得ないのではないかと思います。 R&S はinternet上にいろいろな海賊版が出回っており、どれが正本なのか、科学捜査でもしなければ判定出来ないくらいです。また、追記と脚注がグロタンディーク氏本...

昨年2022年10月以降にコロナヴァイラス対策が緩やかになり、外国人客の来日が増えました。私の欧州某国の知人も久方振りに来日することになり、私が案内兼通訳として同行することになりました。どうしても関西圏にも足を延ばしたいということで、関西在住の友人共にも協力して貰いました。関西訪問中、関西でも屈指の大手私鉄の普通列車に乗ったのですが、私達が着席した座席列の向かいの座席列が私達の座席列よりも短く、乗車扉付近に空間を大きく取っていました。何気なく書かれている日本語を見ると“大きな空間を作るように座席を配置しました”とあり、その下に英語、中国語、朝鮮語等が書かれていました。しかし、その英語を見て私は思わず座席からずり落ちそうになりました。そこには Seats were arranged to make larger spaces . となっており、いかにも機械翻訳でやっつけ仕事をしたことが窺えます。こんな簡単な文章でさえ機械翻訳に頼るなんて小中高生かと思いました。まともな大人(つまり、18歳以上)がやることではありません。隣の海外知人の顔を見るとマースｸ越しでも笑っているように見えました。皆さんはこの英文が何故おかしいか分かりますか? これをおかしいと思わなかったら、平均的知性が無いと言ってもいいでしょう。 先ずおかしいのは Seats が全く限定されていないことです。一般的な Seats 、もっと分りやすく言えば世界のどこでも存在する Seats が大きな空間を作るために配置されるのでしょうか? だから、せめてここでは定冠詞theをつけないとおかしいのです(定冠詞をつけず、 Seats on this train 等のように修飾限定する方法もありますが)。それに伴って larger spaces の方にも定冠詞をつける必要があるのですが、そのまま the larger spaces では見っともなく、また動作の受動態(状態の受動態ではなく)はbe動詞よりもgetを使う傾向が欧米では強く、更に時制も単なる過去形よりも現在完了の方がよく(と言うか、そもそも過去形にすること自体がおかしいのです。この車両の歴史を説明したいのなら話は別ですが、そんな必要があると思わないのが普通でしょう)、元の文を最大限生かすなら The seats have got arranged t...