【翻訳文字起こし全文】チャールズ・ホスキンソンのスピーチ カーネギーメロン大学ホスキンソンセンターのオープニングにて
カーネギーメロン大学に数学研究センターの設立を目的とした2,000万ドルを寄付したと報じられていていますが、そのオープニングでのチャールズ・ホスキンソンの挨拶です。
以下の文章は、IOHKのYouTube動画「カーネギーメロン大学ホスキンソンセンター・オープニングでのチャールズ・ホスキンソンのスピーチ」（2021/9/23）を翻訳文字起こししたものです。
HUNNYプールにステーキングしましょう！
HUNNY：ff5eb7a210b3b322271da7f17753a06d107bda666f34be10017ad723
PoolToolで詳細を見る：こちら
要点
・そこで私は 自分が起業家としていろいろなことをやっていて 数学の世界ではあまり何もできないことを考えると 今世紀中に数学のシステム自体に最大のインパクトを与えるためには何ができるだろうか といろいろ考えました そこで私は 「これまでとは少し違った書き方をすることが重要だ」と答えました
・証明を書いた数学者が死んだら、その背後にある思考、ヒューリスティック、教育的な解説、証明を書くために行った冒険などは、永遠に消えてしまう
Lean Agda Isabelle Coqなど 20世紀に偉大な数学者やコンピュータサイエンティストによってもたらされた素晴らしいツールは ある意味で 数学者が考える方法をコンピュータが理解するのを助けることができます
数学者と対話する知能システムが 実際にそれらのヒューリスティックスや思考パターンを少しずつ吸収し始めるということです
もし不滅のエージェントと一緒に仕事をしたらどうでしょう？作品を読むだけでなく その思考やプロセスを実際に見ることができるのです
それは 未来の数学者にどんな力を与えるでしょうか？
・400人の共同研究者がいて ものすごく技術的なことが書かれています
コラボレーションのためのより良いツールが必要であり 理解するためのより良いツールが必要であり それがLeanのポイントなのです
・最終的には 非常に大きな分散型コミュニティとなり CMUの安全な港を出て アフリカ ヨーロッパ 南米 アジアなど世界中の何百人 何千人もの数学者や数学者になりたい人たちが ここで作られたツールを使って成長し ここで得られた知識を使って成長し まったく新しい数学の言語が進化することになるでしょう
・来年には数学者向けのLeanのようなオープンソースの教科書が出てくるといいですね 数学の言語ができるまでには少し時間がかかるでしょうが
そして後には このパラダイムを使って 数学のすべての分野の教育学全体をカバーし オープンソースの教科書を持つことができるという 素晴らしい瞬間を迎えることになります
ますます多くの人がこのパラダイムに基づいて共同研究を行い ますます多くの人がこのパラダイムに基づいて論文を発表するようになり 雑誌もこのパラダイムに従うようになるでしょう
それはあらゆる種類のものを変え 査読の概念そのものをも変えるでしょう
・アフリカ大陸全体で 現役の数学者は100人にも満たないのです
12億人もの人々がいるのに それほど多くの論文が発表されているわけではありません
それは人々が賢くないからではなく 全く逆なのです
頭が良いのに意志やアクセスがありません
これらのツールがすべての人に役立つものであるならば 象牙の塔から抜け出して 高校や産業界のさまざまな場所に進出するだけでなく 本質的にグローバルなものになることを願っています
・最終的に数学はすべての分野の中で最も包括的なものになるはずです
言語 ジェンダー文化 どれも気になりません
この分野では誰もが平等なのです
本文
MC:Charles Hoskinson氏の登壇を心より歓迎いたします
Charles Hoskinson:皆さん こんにちは
皆さん 来てくださってありがとうございます
感謝しています
経歴を更新しなければなりません
少しでも読みやすくなるようにね
私の旅は素晴らしいものです
私は子供の頃 ホームスクールに通っていました
私はハワイで育ちました
それから高校をかなり早く卒業しました
だから クラスではいつも最年少だったんです
そして 父のように医者になるかどうかを悩んでいました 兄が祖父のように医者になったように それとも 他のことをしたいのか
生物学の授業をすべて受けていながら いつも数学の授業も受けていて 数学の方が好きでした
そのうち 数学の教授になりたいと思うようになりました
それが私の人生の目標です
しかし 私は数学よりもお金の方が好きだということに気づきました
しかし いずれにしても 私は厳密さを保ち 数学の厳格な美しさへの感謝の気持ちを持ち続けました
このような美しく包括的な説明責任を持つ分野は数少ないと思います
評判やブランドは信用できません 例えば 最近ではAtiyahがRiemann仮説を解いたと主張しました
彼はフィールズ賞メダリストであり 大きな名声を得ています
しかし専門家の間では 「じゃあ 証明してみて」と言われてしまいました
病的なまでに懐疑的な人にとって それが数学なのです
それはとても素晴らしいことです
特に組織が信頼を失っている世界では 社会的にも稀なことです
数学はずっとそれを維持しています 私は多くの芸術品を集めていて 1つはJeremyにあげました
バビロニアのプリンプトン322の粘土板のレプリカです
紀元前1800年のものです
そこには ピタゴラスの三角形のカタログが載っています
すごいですね
考えてみてください 約4000年前に 人々はこのようなことを書き留めているのです
そこで私は 自分が起業家としていろいろなことをやっていて 数学の世界ではあまり何もできないことを考えると 今世紀中に数学のシステム自体に最大のインパクトを与えるためには何ができるだろうか といろいろ考えました そこで私は 「これまでとは少し違った書き方をすることが重要だ」と答えました
私たちが現在行っている書き方は 美しい紙を用意して インクをつけて 実際のところ LaTeXで書いてもらうというものです
そしてそれらはコンピュータの中にあります
時には光学式文字認識でデジタル化することもあります
実際に ここにいる何人かの人はそれをしました
そして その背後にある思考 使用されたヒューリスティックス 教育的な解説 それらの証明を書くために行った冒険は失われます
だから 証明を書いた数学者が死んだら それは永遠に消えてしまう
Lean Agda Isabelle Coqなど 20世紀に偉大な数学者やコンピュータサイエンティストによってもたらされた素晴らしいツールは ある意味で 数学者が考える方法をコンピュータが理解するのを助けることができます
そこでの力は 時間をかけて 数学者と対話する知能システムが 実際にそれらのヒューリスティックスや思考パターンを少しずつ吸収し始めるということです もしチャンスがあれば ガウスやオイラー リーマンに会う機会を持つ人はどれくらいいるでしょうか？できませんよね？しかし もし不滅のエージェントと一緒に仕事をしたらどうでしょう？作品を読むだけでなく その思考やプロセスを実際に見ることができるのです
それは 未来の数学者にどんな力を与えるでしょうか？それは コミュニティにどんな力を与えるでしょうか？これは手の届くところにあります
もう一つは 数学は専門性が高すぎるということがあります
トポロジストが代数幾何学者の論文を読めないとしたら それは問題です
その証拠に ABC予想は それが正しいか間違っているかを誰かが言ってくれるのを待っているようなものです 新一は本当に京都を離れたくないのでしょう 彼はあまりにも楽しんでいるせいか 自分の雑誌に掲載しました
問題は 250ページもの証明があるときに 書かれていることをどのようにして知ることができるのか ということです
400人の共同研究者がいて ものすごく技術的なことが書かれています
コラボレーションのためのより良いツールが必要であり 理解するためのより良いツールが必要であり それがLeanのポイントなのです
では なぜIsabelleやMizar AutomathではなくLeanなのでしょうか？
70年代のQEDマニフェストであるAutomathを覚えていますか？Peter Scholzeをはじめとする他の人たちがそれを気に入って 突然 フィールドメダリストたちがそれを使うようになったので 流行になりました
セクシーだし おもしろかったです
数学界は初めてこれらのものを採用することに熱心なようです
私がここにいるのは Kevin buzzardが来たからです
彼はインペリアル・カレッジ・ロンドンの教授で 私たちの社内セミナーで講演してくれたのですが 「ああ Jeremyと話す必要があるし Leanをやる必要がある」と言ってくれました
それが一番の近道です
それで私は「よし」と言って Jeremyに電話をかけて 楽しく会話をしました
そして 彼に教科書を読むためのお金を渡しました
そして私は 「ちくしょう 金はあるんだ 」と言いました
やってやろうじゃないか
センターを建てようと
で これはどこに行くの？まあ 毎年 少しずつお金を足していきます
そして 研究所になるまで基金を増やし続けます
そして最終的には 非常に大きな分散型コミュニティとなり CMUの安全な港を出て アフリカ ヨーロッパ 南米 アジアなど世界中の何百人 何千人もの数学者や数学者になりたい人たちが ここで作られたツールを使って成長し ここで得られた知識を使って成長し まったく新しい数学の言語が進化することになるでしょう
もう少し完全で もう少し特別で もう少し記述的なものです
人間として最後にこれを行ったのは 実はこの大学が設立されたときでした
ここを見てください......1900年だったと思います
David Hilbert 国際数学会議です
彼はこれらの素晴らしい問題を披露しました
彼は 「この問題を解決してください 10年も20年もかかりますよ」と言いました それは非常に楽観的でした
しかし 彼は他の多くの人々と協力していました Gottlob Frege, Bertrand Russel, Alfred North Whiteheadなど 数学の基礎について多くのことを考えていた何十人もの人々と協力して 「数学の原理」のような素晴らしい本を書きました
そして そこに至るまでの1000ページの結論が「1＋1＝2」だったと思うのです
そして残念なことに それらの本のいくつかは少し間違っていることが判明しました
完全性や決定可能性など 彼らが実現したかったことはすべて 思うように実現できないことがわかったのです
しかし それがコンピュータサイエンスの誕生につながったのです
いかがでしょうか
120年以上経った今 私たちはまた同じことを繰り返すことになりました ここカーネギーメロン大学には 頭脳と学生がいます 研究室にいた大学院生たちに会う機会がありました
彼らは素晴らしい経歴の持ち主で 非常に多様なバックグラウンドを持っています
これは 外国人 リーダーシップ そしてこのような素晴らしい人材を引き寄せる部門のリーダーシップの証です 私は自分のチーフスタッフをここに連れてきましたが 彼女の仕事は毎日 素晴らしい人材を見つけてきてくれるように努力することです
自分よりも少しでも優秀な人がいると 私たちはいつも羨ましく思うものです
だから私は 彼らの仕事ぶりをとても誇りに思っています
そして 短期間でこのセンターの成果が目覚ましいものになることを 私はとても誇りに思っています
最初は小さなことから始まります
しかし 大きなものには小さな始まりがあるものです 来年には数学者向けのLeanのようなオープンソースの教科書が出てくるといいですね 数学の言語ができるまでには少し時間がかかるでしょうが
そして後には このパラダイムを使って 数学のすべての分野の教育学全体をカバーし オープンソースの教科書を持つことができるという 素晴らしい瞬間を迎えることになります
そして ますます多くの人がこのパラダイムに基づいて共同研究を行い ますます多くの人がこのパラダイムに基づいて論文を発表するようになり 雑誌もこのパラダイムに従うようになるでしょう
それはあらゆる種類のものを変え 査読の概念そのものをも変えるでしょう
そして10年後 20年後 30年後には指数関数的な成長を遂げ 最終的には業界全体の何十 何百 何千人年もの努力が ここで確立されたものに向けられていくでしょう
では 純粋な数学以外の分野にはどのようなメリットがあるのでしょうか？私たちはソフトウェアの会社でもあります
それが私たちの仕事の核心です IOG 私たちは特殊なソフトウェア企業であり 最大級の学術部門を持っています ワイオミング大学とエディンバラ大学に研究室があり これまで116本がありますが 査読付きの論文をすべて読んでいます
しかし 私たちは形式手法のソフトウェアを書いています
つまり 仕様書を書き コードを書き そのコードが正しいかどうかを何らかのツールやテクニックを使って証明するのです
ここで生まれたアイデアは 演繹法の市場を作るという意味で 商業化することができます
形式手法のエンジニアや数学者が望めば JaredやPolinaが私のために働いてくれたように 実際に雇用を得ることができるのです
彼らの仕事は ただ座って 物の特性を証明したり 仕様書を書いたりすることです
何のためにそんなことをするのか ですか？空から落ちてこない飛行機は好きですか？壊れたいときに壊れてしまう電車は好きですか？爆発しないロケットは好きですか？ソフトウェアはそれに大いに関係しています
ソフトウェアの正しさは 数学的な証明の正しさとある点で同型であり 全く同じタイプの問題であることがわかりましたが 見方が少し違うだけです
そして それを可能にするツールを用意しなければなりません
これらのツールがグローバルに利用できるようになれば 2,540万人の開発者にとって ソフトウェアの書き方が根本的に変わるでしょう
また 「すべての人に」というプレジデントのコメントに対しては このようなツールや技術は フォーチュン500の企業や起業家 博士や数学者だけのものであってはならないと考えています
これらのツールやテクニックが有用であり 社会に影響を与えるためには 幼稚園から12歳までのレベルにまで普及させるべきであり 高校生のカリキュラムの一部となり 問題解決について考える方法の一部となるべきなのです
STEMの問題点は 参入障壁が高すぎることです
だからこそ 多様な人材が育たないのです
文句を言うこともできるし より良いツールで問題を解決することもできます
そして それが究極的にはここで見ていることなのです
まさに 数学の言語について考える能力を与えてくれるものであり どのようにフォーマルであるべきか 何があるべきかを考える力を与えてくれるのです
教育的な解説はどのようなものか？そして あなたの問題解決のアプローチのためのDSLがあるべきだ などです また 一般的な問題についての話し方や 問題解決のためのテクニックやツールをどう考えるかを表現するためにも使われます
私が読んだ最後の数学者で 高校生のために実際に真剣に取り組んだのは George Polyaでした
解き方を覚えている方も多いと思いますが その本がアップデートされて現代風になると嬉しいですね
そして 10年後 15年後 20年後には ここで あるいはコラボレーションのネットワークで行われていることを願っています
最後になりますが 56カ国にある私たちの企業と アフリカにある企業の魂に関して アディスアベバにオフィスがあり 来月アフリカに行くところですが 7カ国 確か5人の国家元首の手本がいます
アフリカ大陸全体で 現役の数学者は100人にも満たないのです
12億人もの人々がいるのに それほど多くの論文が発表されているわけではありません
それは人々が賢くないからではなく 全く逆なのです
頭が良いのに意志やアクセスがありません
これらのツールがすべての人に役立つものであるならば 象牙の塔から抜け出して 高校や産業界のさまざまな場所に進出するだけでなく 本質的にグローバルなものになることを願っています
数学に包括的な説明責任を持たせるという考え方と同じで 最終的に数学はすべての分野の中で最も包括的なものになるはずです
言語 ジェンダー文化 どれも気になりません
この分野では誰もが平等なのです
資格の有無はさておき 全員です
ですから 大陸全体が取り残されているのは意味がありません
CMUを選んだ理由は他にもあり 数年前にKagame大統領と会ったことがあります
私たちがキガリにいたとき 彼が最も誇りに思っていたことの1つは カーネギーメロン大学との共同研究でした 彼はそれについて 「これが成長すればすべてが変わるだろう」と言っていました
そして彼は もっと早くスケールアップできなかったことを嘆いていました
つまり この大学は パイオニアや探検家になるための関与を持っていない人たちに対して すでにコミットメントを示しているのです
ある意味では このセンターのアイデアやコンセプトを 最終的には世界中のさまざまな大学に広げ ハブ＆スポークモデルにしない手はありません
そして その多くはアフリカの大学になるでしょう
皆さん お集まりいただきありがとうございます
知っている人も知らない人もたくさんいますが これは私のキャリアの中でもハイライトと言えるでしょう
私の名前が付いた最初のものです
たまには自画自賛の宣伝をしますよ
そして この先の展開が楽しみでなりません
私はまだ33歳の若造です
だからこそ 10年後 また10年後 そのまた10年後にこの場所に戻ってきて 皆さんのことを知り 自分なりの方法で皆さんと協力していきたいと思っているんです
私のスタッフも何人か連れてきましたが 彼らはそれぞれの分野で伝説的な存在です
ですから ぜひ皆さんも交流して 話して お互いを知り合ってください
お越しいただいた皆様 ありがとうございました
この記事は楽しんでいただけましたか？
↓下のシェアボタンから、Twitterやブログ等でこの記事をシェアしていただけると嬉しいです。
もしよろしければ、HUNNYプールへの委任をよろしくお願いします！