私たちはリーンに固執しているのか？

3年前、私は同僚に非公式な講演を行い、私たちが選んだ証明アシスタントに数学界がその重みを置くことがまだ可能だったDumeyマイクロ秒に生きていると示唆しました。Kevin BuzzardのXena ProjectとPeter ScholzeのLiquid Tensor Experimentのおかげで、Leanはすでにかなりの勢いを得ていましたが、私が講演を行った時点では、Terry TaoはまだLeanを独学しておらず、Mathlibのバージョン3からバージョン4への変換はかろうじて完了したばかりでした。同様に、Lean FROもかろうじて開始されたばかりでした。Leanは今日ほど避けられないものではないように見えました。私の質問は次のとおりです。Leanの代替案を真剣に支援する組織の見込みはありますか？質問をより具体的にするために、Metamathを候補として提案させてください。（明確にしておきますが、私は個人的にMetamathやその他の特定の定理証明器に利害関係はありません。）Metamathには2つの利点があると考えています。数学界がインタラクティブ定理証明器（ITP）に関心を持つ主な理由の1つは、AI生成の証明（あるいは、それどころか複雑な人間の証明）が形式的に正しいかどうかを検証する方法を提供することです。最近の出来事が示しているように、Leanは健全性バグから免れておらず、曖昧な健全性バグを見つけることはAIの得意とするところです。Mario CarneiroのMetamath Zeroに関する研究のおかげで、Metamathを使用する場合、正しさの保証は大幅に高まるでしょう。Metamathは集合論に基づいているため、Leanやその他の主要な候補（Rocq、Agdaなど）が使用する命題型理論の哲学に関して抱く可能性のある懸念の一部に対処することになります。これはJames Hansonの最近のMO投稿で巧みに述べられています。繰り返しますが、私はMetamathに固執しているわけではありません。MizarやIsabelle/ZFも集合論的ITPの主要な候補です（ただし、Metamath Zeroのようなものはありません）。しかし、Leanの人気のかなりの部分が、ごく少数の著名な人々が偶然それを選び、高い注目度を与えたという事実に起因しているのではないかと懸念しています。それは必ずしも、私たちがやりたい仕事にとって客観的に最良のITPであるからではありません。私の考えでは、Leanを支持する最大の議論はMathlibです。他のITPのためにMathlibを複製することは、最近まで実際には不可能に見えていました。しかし、AIモデルが形式数学を書くのがどれほど上手になったかを考えると、他のITPのために同様のライブラリを構築することを考えることはもはや不条理ではないと思います。私は「ムードコード化されたライブラリ」のリスクをよく認識しています。AI生成のLeanコードは現在、Mathlibにとって十分な品質ではなく、同様にAI生成のMetamathコードもMathlibほど良くはならないと期待すべきではありません。しかし、Leanの代替案の可能性をすぐに却下すべきではないと思います。また、Leanを捨てることを提唱しているわけではないことも申し添えておきます。Leanには多くの優れた資質があり、Leanコミュニティは素晴らしいコミュニティであり、破壊されるのを見たくありません。しかし、私は、健全性に対する保証が高く、集合論に基づいた実行可能な代替ITPを持つことが、数学コミュニティ全体にとって良いことであると提案しています。しかし、これには何らかの組織的な支援が必要であり、それがどこから来るのか私にはわかりません。 私は悪魔の代弁者となり、Metamathは物質的な集合論の哲学に関する懸念に影響を与えると述べます。私も特定の定理証明器に利害関係はありません。単に（私の意見では）哲学的な好みを持ち出すことは、証明アシスタントの能力よりも二次的であるということです。Metamathは任意の数学（ZFCとその仲間を通して）を処理できるのであれば、問題はユーザビリティになり、それは別の種類の問題（技術サポート、社会的慣性、開発への投資など）になります。型理論ベースのものも同様です。 証明アシスタントは、証明チェックカーネルと数学ライブラリだけではありません。カーネルの他に、Leanディストリビューションには、並列および増分エラボレーター/タクティックフレームワーク/タクティック/型クラス、多数のフロントエンドの利便性（リンティングフレームワークなど）、ツール（言語サーバー、パッケージマネージャーなど）、ドキュメント（およびドキュメント作成ツール）、コンパイラなどを含むフロントエンドが含まれています。どの証明アシスタントを使用するかという決定は、これらすべてを考慮に入れるべきであり、おそらく、完全に切り替えるよりも、証明の信頼性を高めるためのより安価な選択肢があるかもしれません。 Mathlibと関連ツールに投入されたコミュニティの努力の量は、現時点ですでに純粋数学のためのより良い証明アシスタントを構築できたはずだと信じています。基盤に関する質問はさておき、Leanには、悪いUXとユーザー向けのパフォーマンスの低下につながる多くの設計上の決定があります（つまり、Leanは典型的なハードウェアで操作しているときに顕著に遅くなります）。 公式のLeanカーネルは、Leanカーネルアリーナで最速のカーネルよりも一部で5倍遅いです。その理由は、Leanカーネル自体がLeanで書かれているためです。Leanは、より資金が豊富な最適化作業の恩恵を受けられない実験的なプログラミング言語です。遅くなる理由があるかもしれませんが、中心的な点は、目標が単に高速な証明アシスタントを作成することであり、自己ホスト型エコシステムを持つプログラミング言語を作成することではない場合、証明アシスタントを高性能に構築する自由がより多くあるということです。 David Roberts氏へ。集合論に基づいたITPを使用することが、数学が「本当に何であるか」についての哲学的なコミットメントを伴うとは思いません。依存型理論に基づいたITPを使用することが、数学的対象が「本当に型である」という哲学的なコミットメントを伴うのと同じくらいです。ほとんどの人がITPに求めるのは、「本質的なガイダンス」（Penelope Maddyの言葉を借りれば）を提供することではなく、証明をチェックすることです。集合論と型理論は、この点に関してそれぞれ独自の利点があるため、実行可能な代替案があることは良いことだと思います。 私たちは、インターネットがHTMLとJavaScript（それぞれ互換性のある構造を持つ言語）に「固執」しているのと同じくらい、「リーンに固執」しています。この文脈では、私たちは...