未来の数学ライブラリを構築する

数学者の小さなコミュニティは、リーンを使用して新しいデジタルベースを構築しています。彼らはそれが彼らの科学分野の未来を確保することを望んでいます。

毎日、何十人もの志を同じくする数学者がZulipチャットに集まり、科学分野の未来を形作ると信じていることに取り組んでいます。



彼らはすべてリーンプログラムのファンです。これは、原則として、数学者が証明を書くのを助けることができるインタラクティブな定理証明ツールです。ただし、このためには、数学者はプログラムベースに数学的な規則を手動で入力し、数千年にわたって収集された知識をコンピューターが理解できる形式にする必要があります。



プロジェクトの多くの参加者にとって、その利点はほとんどまたはまったく説明を必要としません。



「基本的なレベルでは、何かがデジタル化されると、それを新しい方法で使用できることは明らかです」とKevinBuzzard氏は述べています。インペリアルカレッジロンドンから。「そして、数学をデジタル化して、より良くするつもりです。」



数学をデジタル化することは古い夢です。この期待されるメリットは、コンピューターで生徒の宿題をチェックするという些細なものから、人工的なインテリジェンスを使用して新しい数学的な発見を行い、古い問題の新しい解決策を見つけるという並外れたものまでさまざまです。数学者は、自動定理証明者がジャーナルに提出された記事をレビューし、人間のレビュー担当者が時々見逃すエラーを見つけ、必要なすべての詳細を証明に記入するという面倒な技術的作業を行うこともできると信じています。



しかし、最初に、チャットで会う数学者は、学校の数学の枠組みの中でリーンに知識を身に付ける必要があり、これまでのところ、このタスクは半分しか完了していません。近い将来、リーンが未解決の問題を解決できる可能性は低いですが、基地で働く人々は、わずか数年でプログラムが少なくとも高校の試験レベルの問題を理解することを学ぶとほぼ確信しています。



知るか？プロジェクトに参加している数学者は、デジタル数学が何に役立つかについて常に明確な考えを持っているわけではありません。



「私たちはどこに向かっているのか正確にはわかりません」とレンヌ大学のSebastienGöselは言いました。

あなたが計画している、無駄のない仕事

夏には、上級リーンユーザーのグループがオンラインセミナー「好奇心旺盛な数学者のためのリーン」を開催しました。最初のレッスンでは、シドニー大学のスコットモリソンが、プログラムを使用して証明を作成する方法を示しました。



彼は、無駄のない言葉で証明したい声明を書き留めることから始めました。人間の言葉では、「素数は無数にある」という意味でした。この主張を証明する方法はいくつかありますが、モリソンは紀元前300年にユークリッドによって発見された最初の証拠のわずかに修正されたバージョンを使用したいと考えていました。証明では、すべての既知の素数が乗算され、1を加算した後、新しい素数が取得されます（製品自体またはその除数の1つが素数になります）。モリソンの選択は、リーンを使用するための基本的なルールの1つに基づいていました：ユーザーは自分で証明の主なアイデアを考え出す必要があります。



「あなたは最初の推測に責任がある」とモリソンはインタビューで言った。



アサーションを入力して戦略を選択した後、モリソンは数分で証明の構造を概説しました。彼は一連の中間ステップを特定しましたが、それぞれのステップは比較的簡単に証明できました。リーンは一般的な証明戦略を提供することはできませんが、小さく具体的な手順を実行するのに役立ちます。証明をアクセス可能なサブタスクに分解すると、モリソンは、普通のシェフに玉ねぎを切るか水を沸かすように指示するシェフのようなものでした。 「これは、リーンが引き継いであなたを助け始めることを望む場所です」とモリソンは言いました。



リーンは、戦術と呼ばれる自動化されたプロセスを使用して中間タスクを実行します。これらは、非常に特定のタスクを実行するために設計された一種の短いアルゴリズムです。



証拠を使って、モリソンはライブラリ検索と呼ばれる戦術を開始しました。彼女はプログラムの数学データベースを調べて、証明の特定のセクションのギャップを埋めることができると彼女が考えたいくつかの定理を返しました。異なる戦術は異なる数学タスクを実行します。それらの1つであるlinarithは、たとえば2つの実数の不等式のセットを取り、3番目の数を含む新しい不等式の真偽を確認できます。aが2で、bがaより大きい場合、3a + 4bは12より大きくなります。連想性などの基本的な代数規則を使用します。



「2年前のリーンでは、連想性を手動で適用する必要がありました」と、バザードでリーンを研究しているインペリアルカレッジロンドンの数学の学生であるアメリアリビングストンは言いました。 -そして、誰かがあなたのためにそれを行う戦術を書きました。使うたびに嬉しいです。」



全体として、モリソンがユークリッドの証明を完了するのに20分かかりました。あちこちで彼は自分で詳細を完成させました。時々戦術家は彼のためにそれをしました。各ステップの後、リーンは、従属型理論と呼ばれる正式な言語で記述された組み込みの論理ルールに対する証明の一貫性をチェックしました。



「それはSudokuアプリのように見えます。間違った動きをすると、ビープ音が鳴ります」とバザードは言いました。その結果、リーンはモリソンの証明の実行可能性を確認しました。



それはとても楽しい練習でした-テクノロジーがあなたのために何かをするときの通常の場合のように。しかし、ユークリッドの証明は2000年以上前から存在しています。今日の数学者の質問は非常に複雑であるため、リーンはまだ質問を理解することができず、ましてやそれらに答えるのを手伝うこともできません。



「このツールが研究に役立つまでには、おそらく数十年かかるでしょう」と、リーンのユーザーの1人であるフォーダム大学のヘザーマクベスは述べています。



したがって、数学者がリーンと協力して本当に興味深い質問に取り組む前に、プログラムに数学のルールを追加する必要があります。そして、これは実際、かなり単純な作業です。





証明作成プログラムの構造：リーンは、作業を検証し、証明のいくつかのステップを自動化することにより、数学者が定理を証明するのに役立ちます。

1）数学者は証明の基本構造を説明し、一連の手順をリーンで書き留めます。

2）数学プログラムのmathlibライブラリには、この証明の手順を実行する一連の戦術があります。数学者はmathlibに新しいデータを追加し続けます。実証済みの定理がmathlibに追加されます。

3）カーネルアルゴリズムは、単純なルールを使用して証明の正しさをチェックします。

*タコはどういうわけかリーンコミュニティの楽しい感情の指定になっています。



「リーンが何かを理解できるようにするには、人々は数学の教科書をプログラムが理解できる形に翻訳する必要があります」とモリソンは言いました。



残念ながら、問題の単純さは、それが簡単に完了することを意味するわけではありません-数学の多くが教科書でカバーされていないことを考えると。

散在する知識

高度な数学を勉強したことがない場合、この領域は正確でよく説明されているように見えるかもしれません。代数、微分計算、数学的分析-すべてがすべてから続き、すべての質問に対する答えが教科書の最後に記載されています。



ただし、学校のカリキュラム、大学のカリキュラム、さらには大学の大部分の数学は、すべての知識のほんの一部にすぎません。それらのほとんどはよく整理されていません。



完全には説明されていない数学の巨大で重要な領域があります。それらは、数学のサブフィールドを人々から学び、それを発明した人々から学んだ少数の人々の頭に保存されています。つまり、彼らは民俗学に基づいて存在しています。



基本的な資料が書き留められている分野は他にもありますが、それは非常に複雑で長いため、誰もその正確性をまだ確認できていません。代わりに、数学者は単に彼を信じています。



「私たちは著者の評判に依存しています。彼が天才で細心の注意を払っている人であることを私たちは知っているので、その証拠はおそらく真実です」とパリサクレイ大学のパトリックマソットは言いました。



これが、定理証明プログラムが非常に魅力的である理由の1つです。数学をコンピューターが理解できる言語に翻訳すると、数学者は最終的に知識をカタログ化し、すべてのオブジェクトを正確に定義する必要があります。



アシアマブビフランス国立情報自動化研究所の彼女は、このような整然としたデジタルライブラリの可能性に初めて気づいたとき、次のように回想しています。プログラムの助けを借りて」。



リーンは、この可能性を秘めた最初のプログラムではありません。最初のAutomathは1960年代に登場し、今日最も人気のあるCoqは1989年に登場しました。Coqユーザーはプログラム言語で多くの数学を形式化しましたが、この作業は分散化され、適切に編成されていませんでした。数学者は自分たちが興味を持っているプロジェクトにのみ取り組み、自分たちの仕事に必要なオブジェクトだけを特定し、多くの場合、それらを独自の方法で説明しました。その結果、Coqのライブラリは、自然に成長した都市の計画のように、雑然として見えます。



「コックは今日、傷のある老人です」と、プログラムに積極的に取り組んでいるマブビは言いました。 「彼は長い間多くの人々に支えられてきました。彼の長い歴史のおかげで、彼の欠点は今ではよく知られています。」



2013年、Microsoftの研究者であるLeonardo deMuraがLeanプロジェクトを立ち上げました。その名前[リーン]は、効率的でクリーンなプログラムを作成したいというdeMooreの願望を反映しています。彼は、このプログラムは数学ではなく、他のプログラムのコードの正確さをチェックするためのツールになるだろうと想定しました。ただし、プログラムの正しさをチェックすることは、証明をチェックすることによく似ていることがわかります。



「私たちはソフトウェア開発に興味があるのでリーンを作成しました。数学の作成とコードの記述には類似点があります」とdeMoore氏は述べています。





リーンユーザーの1人であるフォーダム大学のヘザーマクベス



リーンのリリースの時点で、リーンに最も類似しているCoqを含む、かなりの数の他のヘルパープログラムがありました。両方のプログラムの論理的基礎は、従属型の理論に基づいています。ただし、リーンは最初からやり直す機会を提供します。



彼女はすぐに数学者を引き付けました。彼らはそれを非常に熱心に使用したので、数学の分野での開発についての質問でド・ムーアの自由な時間をすべて取り始めました。 「彼は一流の数学者に少しうんざりして言った-なぜあなたたちは別のリポジトリを作ってみませんか？」モリソンは言った。



数学者は2017年にこのライブラリを作成しました。彼らはそれをmathlibと呼び、それを世界の数学的知識で満たすことに熱心に取り組み、アレクサンドリア図書館の類似物のようなものを作成しました。XXI世紀に。数学者はデジタル化された数学のスニペットを作成してアップロードし、徐々にリーンのカタログを作成しました。また、mathlibは新しいため、Coqのような過去のシステムの制限から学び、資料がどのように編成されたかを追跡することができました。



「モノリシックな数学ライブラリを作成する意図的な試みがあり、そのすべてのフラグメントが相互に機能します」とMacbeth氏は述べています。

アレクサンドリアmathlib

mathlibにプロジェクトのホームページはリアルタイムにプロジェクトの進捗状況を示すグラフがあります。このプロジェクトには、コードの行数でソートされた、最も投資しているリーダーのリストがあります[ちなみに、そもそも、ロシアの数学者Yuri Kudryashov /約です。翻訳。]。デジタル化された数学オブジェクトの総数も計算されます。10月の初めには、18,756の定義と39,157の定理が含まれています。



これらの数学の要素をすべて混ぜ合わせて、リーン内で数学を作成することができます。これまでのところ、一見印象的な数にもかかわらず、それらの範囲は厳しく制限されています。複雑な分析や微分方程式の分野からはほとんど何もありません-そしてこれらは高等数学の多くの分野の2つの基本的な要素です。さらに、このプログラムは、ミレニアム問題（2000年にClay Mathematical Instituteによって「長年解決されていない重要な古典的問題」として定義された数学的問題）のいずれも説明するのに十分な知識をまだ持っていません。



mathlibはゆっくりですが確実に入力しています。作業はチームワークの精神で進行します。 Zulipチャットでは、数学者は形式化する定義を選択し、それらを書き留めるように求められ、他の人の作業について迅速なフィードバックを提供します。



「どんな研究数学者もmathlibを研究して、そこにない40の事柄のリストを作ることができます」とMacbethは言いました。 -それで、彼はこれらの欠点のいずれかを埋めることに決めました。そして、即座の喜びが保証されます-誰かがあなたの作品を読んで、24時間以内にそれについてコメントを残すでしょう。」Sophie Morelが



発見したように、多くのアドオンは小さくなりますオンラインセミナー「好奇心旺盛な数学者のためのリーン」中にリヨンノーマルスクールから。会議の主催者は、参加者に比較的簡単な数学的ステートメントを提供して、実践としてリーンで証明しました。モレルは、そのうちの1人と協力して、彼女の証明にはmathlibにはない補題（小さな中間結果）が必要であることに気づきました。



「それは、何らかの理由でまだそこになかった線形代数からの小さな断片でした。 mathlibを埋める人々はすべてを把握しようとしますが、すべてのオプションを予測することはできません」と、必要な補題を3行ベースに入力したモレルは言いました。



他の貢献はより重要です。昨年、Göselはmathlibのスムーズな多様体の定義に取り組んできました。スムーズマニフォールドは、ジオメトリとトポロジの研究で基本的な役割を果たすセット（線、円、ボールの表面など）です。また、数値理論や計算などの分野の問題でも重要な役割を果たすことがよくあります。ほとんどの数学的研究はそれらなしでは不可能です。



ただし、スムーズなマニフォールドはさまざまな形で隠れることがあります。それはすべてコンテキストによって異なります。それらは、有限または無限の数の次元を持つことができ、境界を持っているか持っていないか、さまざまな数のシステムで定義できます-実数、複素数、またはp-adicのセットで数字。スムーズな多様性を定義することは、愛を定義することに似ています。あなたはそれに会ったときにそれを認識しますが、厳密な定義は、この現象の最も明白な例のいくつかを確実に落とします。



「基本的なことを定義するとき、あなたは何の選択もする必要はありません」とGöselは言いました。 「しかし、より複雑なオブジェクトは、10〜20の異なる方法で形式化できます。」



ゲーゼルは、特異性と一般化のバランスを維持する必要があります。 「私にはルールがありました。マニフォールドの15の異なる用途を定義できるようにしたかったのです」と彼は言いました。 「同時に、私は定義があまりにも一般的であることを望んでいませんでした。さもなければ、それを扱うことは不可能でしょう。」



彼が開発した定義は、1,600行のコードに収まります。mathlibからの定義にはかなりの量ですが、彼がリーンに開いたすべての数学的な可能性と比較すると、おそらくそれほど多くはありません。



「必要な言語ができたので、定理の証明を開始できます」と彼は言いました。



正しい程度の一般性のオブジェクトの正しい定義を見つけることは、mathlibを埋める数学者の主な仕事です。ライブラリの作成者は、今日有用な方法でオブジェクトを定義すると同時に、これらのオブジェクトを今日では予測できない方法で使用できるように十分な柔軟性を備えていることを望んでいます。



「遠い将来に使用するためにすべてが有用である必要性が強調されています」とマクベスは言いました。

パーフェクトイドは練習から生まれます

しかし、リーンは単なる便利なツールではありません。それは数学者に彼らの仕事に再び従事する機会を与えます。マクベスは、証明を書くのに役立つプログラムを初めて試したときのことを今でも思い出します。それは2019年で、プログラムはCoqでした（現在はリーンに切り替わりましたが）。彼女は止められなかった。



「あるクレイジーな週末に、私はこのプログラムで12時間続けて働きました」と彼女は言いました。 「それは本当の中毒でした。」



他の数学者も同様の方法で自分の経験を説明しています。リーンは、コンピューターゲームのようなものだと彼らは言います-ゲームコントローラーを脇に置くのを難しくするのと同じ報酬ホルモンに至るまで。 「これは、1日14時間、疲れを感じることなく、1日中高い状態で行うことができます」とLivingston氏は述べています。 「あなたはいつも前向きなフィードバックを受け取ります。」





SebastienGösel



それでも、リーンコミュニティは、多くの数学者にとって、プログラムに十分なレベルがないことを理解しています。



「形式化された数学の割合を定量化すると、まだ1000分の1パーセント未満しか準備ができていないと言えます」とAIシステムに取り組んでいるGoogleプログラマーのChristian Szegediは、数学の教科書を独自に読んで形式化できることを夢見ています。



しかし、数学者はこの割合を増やしています。今日、mathlibに大学2年生が教えた資料のほとんどが含まれている場合、プロジェクト参加者は数年以内に残りのプログラムを追加することを望んでいます。これは重要な成果です。



「これらのシステムの50年間すべてにおいて、誰も提案したことはありません。座って、研究所の資料を説明する数学の一貫した知識ベースを整理しましょう」とBuzzard氏は述べています。 「私たちは、研究所の試験の質問を理解できるものを作成しています。これは、これまでに起こったことはありません。」



mathlibのコンテンツがリサーチライブラリと一致するまでにはおそらく数十年かかりますが、リーンユーザーは、少なくともそのようなカタログを作成する理論的な可能性を示しています。この目標を達成するには、プログラムコードの形式でデータベースにすべての数学を入力する必要があります。



この目的のために、昨年、ドイツのフライブルク大学のBuzzard、Masso、Johan Kommelinは、この夢の実行可能性を証明するプロジェクトを実施しました。彼らは、基地への研究所の資料の段階的な充填を一時的に延期し、高度な地域に移りました。彼らの目標は、21世紀の数学における最大の革新の1つ、つまりボン大学のPeterScholzeによって過去10年間に開発された「パーフェクトイドスペース」などのオブジェクトを特定することでした。 2018年、彼は彼の作品でフィールズ賞を受賞しました。これは数学で最大の賞です。



Buzzard、Masso、およびCommelinは、少なくとも原則として、リーンは数学者が本当に興味を持っている数学を扱うことができることを実証したいと考えていました。 「彼らは非常に複雑で新しいものを取り、これらのオブジェクトが証明を書くのを助けるプログラムで操作できることを示しました」とマブビは言いました。





Kevin Buzzard



完全な空間を定義するには、3人の数学者が3,000を超える数学オブジェクトの定義とそれらの間の30,000の接続を組み合わせる必要がありました。定義は、代数からトポロジーや幾何学まで、数学の多くの分野に広がっています。それらを1つの定義にまとめることは、時間の経過とともに数学の複雑さが増していること、そしてmathlibの基礎を正しく理解することが非常に重要である理由を示す強力なデモンストレーションでした。



「高度な数学の多くの分野では、学生に教えられるあらゆる種類の数学を知る必要があります」とマクベス氏は述べています。



トリニティは完全な空間を定義することに成功しましたが、これまでのところ、数学者がそれを使ってできることはほとんどありません。プログラムが少なくともこれらの完全な空間が生じる複雑な質問を定式化する前に、さらに多くの数学的定義をリーンに導入する必要があります。



「リーンがパーフェクトイド空間とは何かを知っているが、複雑な分析を知らないのはかなりばかげている」とマッソは言った。



バザードは彼に同意し、パーフェクトイド空間の形式化を「ギミック」と呼んでいます。これは、新しいテクノロジーがその有用性を実証するために時々示されるトリックです。そして今回はトリックがうまくいきました。



「私たちの仕事のおかげで、地球上のすべての数学者が証明を書くのを助けるためにプログラムを使い始めたと考える必要はありません。しかし、彼らの多くはこの可能性に気づき、質問を始めたと思います。」



リーンが数学研究の真の一部になるまでには長い時間がかかるでしょう。しかし、これは今日のプログラムがサイエンスフィクションからの写真であることを意味するものではありません。その開発に関与する数学者は、彼ら自身が線路に乗ることができない場合でも、彼らの仕事を最初の鉄道線路の敷設と比較します-重要な企業の必要な開始です。



「それはとてもクールなことになるので、今日のトラブルに値する」とマクベスは言った。「私は今日それに時間を費やしているので、将来誰かがそれを使って素晴らしい経験をすることができます。」