過去・現在・未来

【「量子情報と通信技術 -- 「量子インターネット」という未来」へのお誘い 】 4月30日のセミナーは、「量子情報と通信技術 -- 「量子インターネット」という未来」と言うテーマで開催します。 この間、量子論・量子情報理論には、「量子コンピュータ」と「量子情報通信」という二つの大きな応用分野があるという話をしてきました。今回は、後者の「量子情報通信」にフォーカスして、特に、その技術的到達点の現状を紹介しようと思います。 量子情報通信では、研究者が実装にしのぎを削っている研究・開発分野は二つあります。一つは、量子暗号とその量子キー配布の実装で、もう一つは、量子テレポーテーションの実装です。いずれの分野でも、近年大きな進展があります。そうした動向を紹介するのが、今回のセミナーの目的です。 セミナーは、次のようなトピックを取り上げます。基本的には、代表的な論文の紹介というスタイルで構成しようと思っています。 【量子暗号と量子キー配布】 日本も頑張っているこの分野では、2021年の1月に、中国の研究チームが、Nature誌に投稿した論文の概要を紹介します。彼らは、光ファイバーだけでなく衛星も使って、宇宙と地上を統合する 4,600kmに及ぶ、量子キー配布のネットワークを実装しました。 【量子テレポーテーション】 この分野では、2020年の7月に、アメリカの研究チームが arXiv に投稿した論文を紹介します。彼らは、22km離れた地点を光ファイバーで結んで、90%以上の信頼性で安定的に量子テレポーテーションを行うことに成功しました。 【量子リピーター】 量子通信の技術的なネックの一つは、現在の光通信で利用されている中継増幅器は、量子の状態を壊してしまうので、そのままでは使えないことです。量子の状態を壊さない中継器を「量子リピーター」と言います。この分野の取り組みの現状と課題を紹介します。 【量子インターネット】 興味深いのは、量子通信技術の着実な発展の中で、「量子インターネット」の構想が立ち上がりつつあることです。最初は、小さな動きでしたが、近年は大きな流れになりつつあるように思います。セミナーでは、「量子インターネット」と言う言葉を、多分、最初に使ったと思われる、2008年のarXivへの投稿論文を紹介します。 インターネットの未来については、現在、さまざまな議論がありま

【 Open-AI Theorem Proverの限界 】 セミナーは今日なのに、大事なことを書くのを忘れていました。 というか、途中で、セミナーの構成を変えたのですが、その時、先に作っていたショートムービーの公開を飛ばしてしまっていることに昨日になって気づきました。公開資料もその部分を埋めたものに更新しましたので、改めてアクセスください。 どたばたしてすみません。 抜けていたのは、Open-AI Theorem Proverのチームの論文の結論部分の紹介です。 彼らは、率直に、Open-AI Theorem Proverの証明能力には限界があることを認めています。その評価は、妥当なものだと思います。 「現在のその主要な限界は、二つあるいは三つ以上の自明ではない数学的推論をつなげていくことの無能力さにあると考えている。このことが、（例外的にではなく）整合的に数学オリンピックの問題に挑戦することを妨げている。」 「複雑な推論ステップを必要とする証明の多くは、現在のコンピュータの能力の地平を超えたところにある。我々が、たとえ挑戦的な数学オリンピックの問題のいくつかを解いたとしても、我々のモデルは、いまだこれらの競技の最も優秀な学生たちと競争するにははるかに遠い場所にいるのである。」 【「Open-AI Theorem Prover -- 論文の結論にみるその「限界」の認識」を公開しました 】 https://youtu.be/ICkF3ocX5JI?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/12HljpZNPJl6b0G2XUDbhnka1wlndjavn/view?usp=sharing セミナーの申し込みは、本日のセミナー開始（19:00）まで受け付けています。 https://math-proof.peatix.com/ このトピックのまとめページは、こちらです。 https://www.marulabo.net/docs/math-proof/

【 3//26 マルレクの講演資料公開しました 】 3/26 マルレク「コンピュータ、数学の問題を解き始める」の講演資料を、MaruLaboのページ  https://www.marulabo.net/docs/math-proof/   で公開しました。ご利用ください。 講演資料は、次のURLからも直接アクセスできます。 https://drive.google.com/file/d/12726t4yD0ouUngmFXSy2UIzvQptSdP6g/view?usp=sharing 【 3/26 マルレクの申し込み受付中です！ 】 3/26マルレクのお申し込みは、次のページから受付中です。 https://math-proof.peatix.com/

【 数学のスタイルが変わる? 】 Voevodskyが危惧したことは、数学は、累積的（accumulative）な性格を持つので、そこに誤りが紛れ込むと、誤りも累積する危険があるということでした。彼は、それを数学の危機だと考えます。 彼は、数学への誤りの混入を避ける唯一の道は、数学の証明を、コンピュータで検証できるプログラムの形にすることであると考えるに至りました。ただ、その当時（もう21世紀に入っていたのですが）、そうした彼の考えを支持する数学者は、ほとんどいなかったと言います。 2010年頃から状況は変わり始めます。Voevodskyが提唱するHomotopy Type Theory に基づく数学の新しい基礎づけ Univalent Foundationが数学者の注目を集め始めます。2012年から2013年にかけて、プリンストン高等研究所は、"Special Year"を設定し、Univalent Foundationについての大規模な連続セミナーを開催し大きな成功をおさめます。数学者の関心は大きく広がりました。 Univalent Foundationは、数学理論として新しい内容を持つのですが、それらの理論の形式化をコンピュータ上の証明支援システムで行うことに適しているという特徴があります。特筆すべきは、Voevodsky は、Univalent Foundationに基づく数学の基礎づけ・再構成を、彼の主張に忠実に、GitHubで公開されたコンピュータ・プログラムの形で実行して見せたことです。こうして、それまで、数学でのコンピュータ利用に懐疑的だった多くの数学者の見方は変わり始めます。 コンピュータ上の証明システムは、個々の数学的証明の正しさの検証に使えるだけではありません。大規模な数学の形式化を整備することで、数学者のコミュニティが、形式化された定義や定理や証明を共有し、検索可能なライブラリーを構築することを可能になることを、数学者は気づき始めています。 21世紀の数学のスタイルは、今とは違ったものになっていくでしょう。 【 「Univalent Foundation」を公開しました 】 https://youtu.be/1zm8E2Y7vyY?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのp

目の前から、人間が作ったもの、人間に関わるものを、すべて消してみましょう。それでも、自然はあるがままの姿で、広がっているように思えます。野に咲く花も、空を飛ぶ鳥も、木々をゆらす風も、夜空の星も。 ただ、そうした空想を行うことが、だんだん、難しくなっています。人間のいない世界のイメージといえば、「廃墟」のイメージを持つ人がむしろ多いかもしれません。それでも自然は残ると僕は思うのですが。それは、私たちの日常的な視界から、自然が見えにくくなっているからだと思います。 一方で、現代は科学の時代だと多くの人が考えています。ただ、科学の主要な対象である自然から、私たちは、どんどん遠ざかっています。そのことは、自然に対する関心だけでなく、いずれ、科学に対する関心をも失わせる力として働くことになると感じています。 科学を私たちにとって疎遠なものにする、もう一つの大きな力があります。 それは、そもそも、科学が歴史的には、冒頭に述べたような素朴な自然観から、自分を意識的に分離することで生まれたことによるものです。 私たちの遠い遠い祖先は、自然と深く結びついていました。というより、圧倒的な自然の力の前に人間は無力でした。ただ、自然に対する畏怖・感嘆の念を持ち得たことは、人間を他の動物とを区別するものです。それは、その後、宗教・芸術・科学等に枝わかれしていく、すべての人間の営みの原始の共通の起源になりました。 時間を何万年か進めます。話は少し飛躍します。 現代では、科学は、主要に「科学者」という専門家集団によって担われています。彼らは、特殊な訓練を受け、特殊な言葉で話します。その言葉は、一般には、わかりにくいものです。 「科学者」が人口に占める割合は、大きなものではありません。おそらく宗教が支配的であった時代、どの村々にも必ず存在していた神職者が人口の中で占めていた比率を上回ることはないと思います。 （科学の世界では、博士号を取得した科学者の卵たちの「過剰」に悩まされています。それは、社会的には「構造的な問題」なのですが、僕は、むしろ、歴史的には必然的な傾向のように考えることができると思っています。） それでは、なぜ、多くの人は、実際にはかなり疎遠なものでしかない科学に対して、現代は「科学の時代」だと考えるのでしょう？ その理由は、明確だと思います。「科学」の応用としての「技術」が、現代の

【 巨人の肩の上の小人 】 「フェルマーの定理」を証明したワイルズは、自分を「巨人の肩の上の小人」に喩えました。それは自分の仕事は先人たちの偉大な業績の上に成り立っているという謙遜なのですが、同時に、そのことは彼が数学という知の特徴をはっきりと自覚していることを表しています。 数学的知には、人間の認識によって獲得されたものとしては、独特の性質があります。それは、いったん数学的に「真」であることが証明された定理は、時代が変わっても場所が変わっても、ずっと「真」のままであり続けることです。それを数学的真の「普遍性」とか「不変性」ということがあります。 そうして獲得された知は、個人というよりは人類の知として蓄積されていきます。それを数学的知の「累積性」といいます。 先に、数学者がコンピュータによる形式的証明を受容する動きが広がっている理由をいくつか見てきたのですが、最後にあげた 　「数学者は、しばしば「間違った証明」する」 というのが、結局は一番大きな理由になるだろうと僕は考えています。 偽である命題からはどんな命題も導くことができます。「間違った証明」も、誰もそうと気づかなければ、それを利用して導かれる真である保証のない「証明」も共に「蓄積」していきます。 それは、がっしりして盤石であると思われた「巨人」の足腰が、徐々に蝕まれて行くことを意味します。病んだ巨人の肩の上では、小人たち（僕らのことです）は、自由に遊ぶことはできません。 ただ、数学者も一般の人も、あまりそのことを深刻に考えていないようにも見えます。 　「専門性の高い数学者が証明を誤ることは、ほとんどない。」 　「数学者だって人間だもの、誤ることだってある。」 数学者の誤りの問題を、数学の基礎である累積性への脅威として捉えたのは、Voevodsky が始めてだったと思います。彼は、数学の形式的証明の必要性を強く訴えます。 【 「 数学的知の「累積性」」を公開しました 】 https://youtu.be/9NIcuPvrDj0?list=PLQIrJ0f9gMcPP8LOejaQQlYufAMEQbcdg スライドのpdfは、次からアクセスできます。 https://drive.google.com/file/d/1-79tELOCp2Cpmo-pTIAwg7U7ow4X8LTS/view?usp=sharin

【 数学者も証明を間違える 】 では、なぜ、数学者はコンピュータを使い始めたのでしょうか？  それには、理由があるように思います。 第一の理由は、人間の手にはあまるが、コンピュータなら解ける巨大なサイズの問題が存在するからです。一般的な解法は見当たらなくても、場合の数が有限なら、すべての場合をしらみつぶしに総当たりでチェックができるなら、問題を解くことができます。 数学の証明問題へコンピュータが最初に使われたのが、こうした方法が使われた「四色問題」であったことは象徴的です。このことは、コンピュータを使って、そういうタイプの問題に、人間がチャレンジすることが可能になったのだとも言えます。前回見たヘイルズの「ケプラー予想」の証明も、こうしたタイプの証明でした。 ただ、場合の数が有限だとしても、シラミつぶし総当たりの方法が、実際にコンピュータで実行可能とは限りません。このタイプの問題は、たくさん存在するのですが、実際にコンピュータで解けるのは、場合の数が小さい時だけです。 さらに、難しい数学の問題がすべてこのタイプである訳ではありません。むしろ、数学者の多くが取り組んでいる問題は、こうしたタイプの問題ではないのです。ですから、数学者が証明にコンピュータを使い始めたのには、別の理由があります。 第二の理由は、証明が複雑になると、証明が正しいことが検証しにくくなるからです。先に、証明が長すぎて、「その証明を、全部読んでいる数学者は誰もいない。」というブラック・ジョークを紹介しました。先に紹介した「Feit–Thompson定理」の証明は、このケースです。 　「そうだ。コンピュータを使った巨大な証明なんか信用できない。誰がその正しさを保証するんだ。」　 確かにその通りです。ただご安心を。現代の巨大証明は、検証ずみの証明支援システムを利用して、それ自身の正しさを検証しながら、証明を実行します。その意味では、1970年代にアッペルとハーケンが行った「四色問題」の証明と、21世紀になってからのゴンティエによる「四色問題」の形式的証明とは、本当は異なるものです。 証明の長さだけが、問題ではありません。例えば、全く新しいアイデアに基づく証明は、その正しさを（彼が数学の専門家であったとしても）第三者に確信させるのは難しいのです。 ペレルマンは、2002年から2003年にかけて arXiv