昨年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 to make the spaces larger. くらいでいいでしょう。もしくは、もっと説明的にするならばThe number of seats on this train has been reduced to make the spaces larger. とするのがいいのではと海外知人に言ったところ、英文がどうのこうの言う前に、そもそもそういう、どうでもいいような説明が少しでも無いと困る日本人がいるのかと疑問に思ったようで、Who needs such a useless explanation at all? Perhaps, nobody looks at it.と言われました。確かに、そんな説明が無くても誰も文句を言わないでしょう(そう思いたいです)。海外知人は言い過ぎたと思ったのかどうか分かりませんが、Shall we tell the railway company that? と言ってくれましたが、それに対してNo, let's not. It's useless to do so because most Japanese aren't good even in English and because it's impossible for there to be no trouble regarding English in Japan. Such a kindness gets called "お節介" in Japanese, which means meddling, and it gets disliked in Japan. と答えました。このままでは、この大手私鉄の面目が丸潰れなので、名誉回復のためにTo be fair to this railway company, well-known mathematician Kiyoshi Oka used to get on the trains of the railway company while living in Wakayama prefecture during the 1940s. At that time, he risked his life to do maths. と言うと、海外知人は暫く胸に手を当てて黙とうしました。ここまで書くと、この時私達がどこにいて、どの私鉄を利用したか分かる人は分かるだろうと思います。
さて、前置きはこれくらいにして、今日紹介する記事はQuantaのProof Assistant Makes Jump to Big-League Mathです。何故、この記事を選んだかと言うと、皆さん御存知のペータ・ショルツェ博士が証明に対して実に真摯なことが分かるからです。そして、多忙にも拘わらず、協力すべき時は十分に協力をしてくれますので、さすが世界のリーダだと思います。日本の誰かさんとはえらい違いです。因みに前置きの海外知人はショルツェ博士のことを何年も前(勿論Fields賞受賞よりずっと前です)からI'm sure he'll make one of the greatest mathematicians in the maths annals. と言って非常に尊敬してました。ともかくも、その私訳を以下に載せておきます。
[追記: 2023年01月24日]
同じ話題を扱ったものに“数学者達は‘大統一’理論におけるコンピュータ支援の証明を歓迎する”があります。
[追記: 2023年02月03日]
上述の英語に関する前置きには後日談があります。私から話を聞いた関西在住の友人がその後、問題の私鉄大手の電車に乗ったところまたまた変な英語に出くわしました。昨今のパァンデミｸ予防のために、各車両のどこかの窓が開いたままのことが普通だと思いますが、友人が開いたままの窓を見るとそこには日本語で“窓を開けて換気しています”と注意書きがあり、その下に英語でWe open this window and ventilating. と書かれていたそうです。これには友人も呆れ果て、やっぱり日本人は頭悪いのんとちゃうかと関西弁丸出しで言ってました。少し解説すると、先ずventilateは他動詞なのにも拘わらず目的語がありませんし、そもそも何故ventilatingという現在分詞なんでしょうか。現在進行形にしたかったのか、それとも分詞構文のつもりだったのか、意味不明です。私なら素直にWe've opened this window to ventilate the train. とするところです。
話は変わりますが、殆どの日本人は有声音、無声音の違いさえも理解してません。それが証拠に関西には戦前から絶大なる人気を誇る○○タイガースと呼ばれる球団がありますが、タイガーズなら兎も角もタイガースって何ですか？それだけじゃなく、挙げれば他にもきりが無い程多くの実例があります。“やっぱり日本人は頭悪いのんとちゃうか”はあながち間違いではないのかも知れません。
証明支援系が一流数学へと飛躍する
2021年07月28日 Kevin Hartnett
数学者達はコンピュータプロゥグラァムLeanを使用して数学研究の最先端における難しい定理の正しさを検証して来ている。
コンピュータ証明支援系は長年数学において興味をそそる腋筋だった。つまり、数学者達がどのように研究するかの中心的な側面を自動化する期待はあるが、実際にはその方面に効果が殆ど無かった。
しかし、06月の始めに完了した新しい結果は大リーｸﾞにおける新人の最初の安打の感触を持つ。すなわち、ついに証明支援系が複雑で現代的な証明の正しさを検証することで数学研究の最先端に真の貢献をした。
“それは現代数学が定理証明系の中に定式化出来ることを示している”とBhavik Mehtaは言った。彼はケィンブリヂィ大学院生だが、その研究に貢献した。
問題の証明はボン大学のペータ・ショルツェによるものである。彼は世界で最も広く尊敬されている数学者の一人である。それは“condensed mathematics”と呼ばれる、彼とコウペンヘイゲン大学のDustin Clausenが数年間取組んでいる大きな計画の一環に過ぎない。
彼等の目標は位相に対する新しい基礎を造ることだ。つまり、伝統的な位相空間(その実例は球体やドゥナッを含む)の概念を彼等が凝縮集合と呼んでいるもっと汎用的なオブジェクッに置換えることである。この新しい見方において、位相空間は糊付けされた粉塵の塊りの無限個の点々から集積されていると考えられる。
その計画は、ショルツェが2019年07月に一週間かかって考え出した、特に重要で難しい証明を含んでいる。それは位相空間を凝縮集合で置換えても、まだ実解析と呼ばれる数学の分野が成立することを証明している。
ショルツェは月曜日に証明を始めた。彼はコンピュータを使わないことは勿論のこと、めったに何も書かず、完全に彼の頭の中で研究した。木曜日の午後までに、彼が確信を持てなかった一つを除いてほぼ解決した。そんな複雑な議論を記憶の中で保持するために必要な一心不乱の集中力の緊張も彼は感じた。だから、その夜彼は友人達と酒場でくつろいだ。翌日金曜日に彼はその代償を払った。
“私は完全に二日酔いになった”とショルツェは言った。
だが、週末を超えて研究する時間が無いことも彼は分かっていたので、証明を完了するために金曜日を最良の機会にしなければならなかった。過去一週間に渡る、彼の頭脳の中で構築されていた全ての事柄に疎くなっていて、そして再び月曜日に新たに始めなければならない思考は彼が願っていたものよりも大変だった。
“頭脳の中で再びこれを再構築するための精神的容量を私は持っていないと思った”とショルツェは言った。
だから彼は力尽くで乗越え証明を終えた。だが後に、彼がやったことが正しいのか確信が無かった。彼が最後の障害をクリヤした朦朧とした状況よりも大変であることが理由だった。証明がとても複雑なのでショルツェは何かを見落としている可能性があることも分かっていた。
“それは多くの動く部分を持つ、非常に入り組んだものだ。これらのパラァミタの一つを変える時、どの部分がどれくらい動くのかを知ることは困難だ”とショルツェは言った。
ショルツェは2019年11月まで証明を実際に書下す時間が見つからなかった。一年後、彼はImperial College Londonの数学者であり、Leanと呼ばれる証明支援プロゥグラァムに対する有名な伝道者であるKevin Buzzardに連絡を入れた。ショルツェは彼の証明をLeanの中に打ち込む(ソフトウエアプロゥグラァムのような符号の列に変換して)ことが可能なのかどうか知りたかった。そうすることでプロゥグラァムが証明の正しさを検証出来るであろう。
Buzzardはショルツェの質問をJohan Commelin(Freiburg大学の博士号取得後の研究者)を含む、Leanコミュニティの少数メンバに伝えた。Commelinはその作業に対する完全な知識を持っており(彼は数年間Leanを使用していて、condensed mathematicsに詳しかった)、ショルツェの証明を検証することが数学コミュニティにおける証明支援系の地位を高めるであろうと確信した。
“そのような計画においてショルツェと共同研究出来ること、その研究に彼の名前が付加されることはLeanにとって大きな押し上げになるであろう”とCommelinは言った。
しかし、彼もそれをすることは一年かそれ以上かかるであろうと考えて躊躇した。Commelinは証明を検証することに全時間を費やすかも知れず、結局の所、他の数学界はただ肩をすくめるだけであろうと懸念した。
“私がこの研究に2年間費やし、洞窟から出て私が‘これは申し分ない’と言うならば、他の数学界は‘うわお、私達はショルツェが証明したことを既に分かっていたよ’と言うだろう”とCommelinは言った。ショルツェ自身が完全には確信しなかったことが問題ではなかろう。
だから、Commelinはショルツェに研究の重要性を保証する公式声明を自ら出してくれないかと頼んだ。ショルツェは賛同し、Buzzardのブロｸﾞにおいて2020年12月05日に投稿した。
彼等は研究を“Liquid Tensor Experiment”と呼んだが、証明の中で使用される、流体実ヴェクタ空間と呼ばれる数学オブジェクッに対する黙礼であり、ショルツェとCommelinが楽しんでいるLiquid Tension Experimentと呼ばれる前衛的ロｸ集団に対する会釈だった。4,400語の手引書の中で、ショルツェは結果の技術的側面を説明し、コンピュータによる検証の重要性について彼が分かったことを平明な言葉で保証する注記を付け加えた。
“私はこれが現在まで私の最も重要な定理かも知れないと考えている(今のところ何らかの応用をあまり持たないが、これが変わるだろうことを確信している)。それが正しいことを確認した方がいいでしょう...”とショルツェは書いた。
保証を準備出来て、Commelinは仕事に取り掛かった。彼が特に証明をプロゥグラァムに検証して欲しい数学命題をLeanに説明した後に、彼は更に多くの数学者達を計画に連れ込んだ。彼等は最もアプロゥチし易そうな少数の補題(証明の中の途中段階)を特定した。それらを定式化し、符号化して数学知識ライブラリ(それをLeanは与えられた命題が真かどうかを決定するために利用する)に加えた。
昨年の10月にQuantaはLeanに数学を書く集団的努力は“納屋を建立している雰囲気”を持つと書いた。この計画でも何ら異ならない。Commelinは証明の個々別々の部分を特定し、それらをZulipによく投稿した。ZulipはLeanコミュニティのための中心として役目を果たしている議論掲示板である。数学者達が彼等の専門知識に一致する証明の一部分を見た時、彼等はそれを自発的に定式化したものだった。
Mehtaは研究に貢献した約12人の数学者達の一人だった。05月に、彼はGordanの補題と呼ばれる命題の証明の定式化を手伝ってほしいというCommelinの投稿を見た。Gordanの補題は組合せ幾何学においてMehtaの研究と関係した。数学者達が構築しているより大きな証明の部分と一貫性を持つ言葉で証明を符号化するのに彼は一週間を要した。それはLeanが動くやり方の象徴だったと彼は言った。
“一つの巨大な記念碑を作製するために多くの人々が彼等の得意なことをする一つの大きな共同作製である”と彼は言った。
作業が進むにつれ、ショルツェはZulipに常駐し、疑問に答え、証明の複数部分を説明した。つまり、建築現場で建築業者達に指示を出す建築設計者にちょっと似ている。“彼はいつもそばにいた”とCommelinは言った。
05月の終わりに、ショルツェが最も確信を持てなかった証明の一部分の定式化をグルーﾌﾟは終えた。05月29日午前01時20分にCommelinは最後のキー打ち操作を入れた。Leanは証明をコンパイルし、機能しているプロゥグラァムのように走り、ショルツェの証明が100%正しいことを検証した。それらのテクニーｸが新しい場面設定で本当に動くだろうことが分かったので、今やショルツェと他の数学者達はそれらを実解析から凝縮集合へと適用出来る。
そして、ショルツェがまだ頭の中で証明を考え出すことを好む一方で、Leanの能力は彼を感心させた。今、彼は数学研究における恒久的な役割を行うプロゥグラァムを予測出来る。
“この実験は証明支援系が如何に有能であるか私の印象を劇的に変えてしまっている。やって欲しいものが何であれ、それをLeanに定式化することが大体において賢明であると私は今考えている。現実の障害は無い”とショルツェは言った。
コメント