数学のすべてを形式化する方法

数学のすべてを形式化する方法 投稿日: 2026年10月16日 by xenaproject (これはゲスト投稿で、Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash、Adam Topazによって書かれました) 先週のOpenAIの大規模リリースに対する数学者たちの反応は、興奮から不満まで様々ですが、一つだけ確かなことがあります。AIは、形式的にも非形式的にも、定理を証明する上で驚くほど優秀になったということです。形式分野での成功は、AI愛好家たちに、将来の世代への遺産として、今こそ数学のすべてを形式化する時だと宣言させています。私たちはこの提案に共感します。私たちは数学的推論における新技術の力を認識し、私たちが知っていて愛しているこの分野にそれらが貢献できることを評価しています。私たちはAIが果たす役割について一般的に楽観的ですが、できるだけ早くすべてを形式化するという最近のいくつかの呼びかけには深く懸念しています。うまく行われれば、大規模で協調的な形式化の取り組みは、数学的探求と発見を著しく拡大することができます。うまく行われなければ、それはせいぜいリソースの無駄であり、より可能性が高いのは、永続的な損害を与えることです。私たちは形式化がうまく行われることを望んでいます。したがって、この記事では私たちの懸念を明確にし、AIと形式化に関する私たちの経験の一部を説明し、すべての、あるいはほとんどすべての数学的定義、定理、証明が形式的な表現を備え、これらの成果物が数学の繁栄を助ける世界に向けて、私たち全員がどのように協力できるかについての前向きなビジョンを提供します。 AIが数学で果たす役割が今日、論争の的となっているのと同様に、形式化におけるその役割もまた論争の的となっています。AIに対する専門的な形式化担当者の間での態度の範囲は、より広範な数学者の間での態度の範囲と同じくらい広いです。私たちは、私たちが価値を置き、尊敬する意見を持つ、私たちの最も親しい友人や同僚の何人かが、AIを使用した大規模な形式化に強く反対していることを認識しています。ここで私たちが述べることは、私たちが所属する組織やコミュニティのいずれかの見解を代表するものと見なされるべきではありません。 懸念 まず、形式的な成果物が誰もそれを使用しなければ、それほど価値がないという観察から始めましょう。昨年2月にMath, Inc.がMaryna Viazovskaの高次元球充填の結果を形式化するプロジェクトを乗っ取ろうとしたとき、それは技術が何ができるかを印象的に示しましたが、それ以上の貢献は数学にはありませんでした。元のプロジェクトチームは、8次元の結果の質の高い形式化を準備し続け、AI生成コードのクリーンアップは、それに見合う以上の手間がかかることをすぐに発見しました。コードを破棄して、AIの十分な助けを得ながらも、正しくやり直す方が良いことが判明しました。AnthropicがClaudeが11日間で書かれた1300万行のコードでフェルマーの最終定理を形式的に検証したと発表したとき、Kevin Buzzardは結果を陽気に称賛すると同時に、より現代的な証明の形式化を継続するつもりはないと宣言しました。ここでも、達成は印象的ですが、このAI生成コードはおそらく継続的な価値はほとんどありません。 定理は真剣に疑われていなかったため、形式的な成果物の価値は、単なる正しさ以上のものから得られるものにのみあります。私たちは、形式化を使用してより多くの数学を行い、それらなしではできなかったよりも良く行うために、すべてを形式化したいのです。私たちは可能な一般化について考え、異なる数学分野間のつながりを探索し、予期しない応用を検討したいのです。私たちは知識をリファクタリングし、改善したいのです。手動形式化の喜びの一部は、概念をよりエレガントに、より効率的に、そして目的に適したものにするために調整できることを認識することから生まれます。知識は、理解に貢献するまで価値がありません。形式化の価値は、データを使用し、対話する能力から生まれます。 OpenAIが有限時間で爆発するナビエ・ストークス方程式の解を発表したとき、自然言語の証明にはLean形式化が伴いました。以前の例とは対照的に、ここでは正しさの信号が重要な役割を果たしました。自然言語の証明はほとんど理解不能ですが、解が正しいことにはほとんど疑いの余地がありません。それにもかかわらず、OpenAIは、結果をどのように得たか、アイデアの出所とクレジット、そして正しさだけに焦点を当てることが、ミレニアム賞が育むことを意図した探求と理解を discouragedしたという懸念から、数学コミュニティの怒りを引き起こしました。したがって、ここでも、飾り気のない形式的な成果物は諸刃の剣です。OpenAIの後のダンプには、驚くべき重要な数学が含まれていますが、同時に読者や理解の構築に対する著しい無視を示しています（いくつかの結果は撤回されており、多くの非形式/形式のペアは微妙または重大な方法で逸脱しており、非形式の書き込みのほとんどは impenetrableです）。これが私たちの懸念を説明しています。数学を形式化するために数百万ドルを費やすことが、誰も使用しないライブラリにつながるなら、それはリソースのひどい無駄になるでしょう。さらに悪いことに、このプロジェクトは良い研究とAIの生産的な使用を discouragedし、研究が依存する社会規範と慣行を混乱させ、この分野を数十年後退させる可能性があります。壮大な失敗は、後で回復することを困難、あるいは不可能にするでしょう。既存の結果の質の悪い形式化は、形式化がないことよりも悪いのです。 ポジティブな側面 大規模な研究所からの成果の一部はうまく行われました。OpenAIの単位距離推測に関する作業と、Anthropicのリマンゼータゼロの密度に関する作業は際立っています。それらは印象的な新しい能力を示し、理解に貢献し、コミュニティはその後それらの作業に基づいて構築しました。これらは、研究所が積極的に貢献できる方法の例であり、研究コミュニティと研究所との間のさらなる建設的なパートナーシップを奨励します。良い形式ライブラリは、数学研究の未来に対する私たちの前向きなビジョンを可能にするでしょう。人間、AI、そしてLean言語は協調して機能します。今日、AIは数学研究の多くの側面で非常に有能です。インタラクティブな定理証明器を使用している研究者は、証明の妥当性をチェックできるコンパイラを持つことの力をすでに理解し、高く評価しています。これらのツールを組み合わせると、信じられないほど効果的です。AIは作業中に形式証明を生成し、それらをLeanコンパイラに対して常にチェックし、不正確な推論を自動的に削除します。このビジョンを実現するには、前例のない規模で、高品質で包括的な形式化された数学のライブラリが必要になります。これにより、数学者は研究の最前線で効果的に作業できるようになります。私たちは研究数学者として書いていますが、このビジョンは数学を超えて広がり、工学や科学の研究を加速させる可能性があることを念頭に置かなければなりません。もし、そしてただ、私たちがそれを正しく行えば、その見返りは非常に大きなリソース投資を正当化するでしょう。 これまでの教訓 AIを形式化の支援に利用したいのであれば、アライメント問題の特殊なケース、すなわち、形式ライブラリがコミュニティの数学的目標を満たすことを保証するという問題を解決する必要があると主張してきました。このケースを解決することが、AIを安全で信頼性が高く、私たちの価値観をサポートする方法で、より一般的に利用する方法についての強力な教訓を提供すると信じています。どうすればそれができるでしょうか？私たち誰も確実には知りません。それがフロンティアでの生活をエキサイティングで不安なものにしている部分です。しかし、集合的に私たちは形式化のためのAIの使用経験があり、真剣な取り組みはこれまでに学んだことに注意を払うべきです。特に、以下のプロジェクトに注意を喚起したいと思います。Mathlibは、形式数学エコシステムをサポートするオープンソースのコミュニティ主導のライブラリであり、2026年のJean-Pierre Demailly Prize for Open Science in Mathematicsを受賞しました。これは、65人のレビュー担当者とこれまでに950人の貢献者によってキュレートされています。