人工知能（AI）がソフトウェア開発に与える影響は広く議論されてきましたが、私がまだあまり見かけない視点があります。私は、AI が形式的検証（formal verification）—数十年にわたりニッチあるいは周辺領域と見なされてきた技術—を本格的にソフトウェア工学の主流へと導くと信じています。
Rocq、Isabelle、Lean、F*、Agda といった証明支援ツール（proof assistants）や証明指向プログラミング言語は長年存在しています。これらは開発者がコードに対して形式的な仕様（specification）を書き、すべての状況（想定外の奇妙な境界条件も含む）でその仕様を満たすことを数学的に証明できるようにします。これらのツールは、OS カーネル、C 言語コンパイラ、暗号プロトコルスタックなど、大規模な形式的検証ソフトウェアシステ
AI+ 形式化証明 は数学界の働き方を変えている
陶哲轩（Terence Tao） は複数の記事、ブログ投稿、講演で、Martin Kleppmann と非常に似た見解を示している：AI は形式検証（formal verification）と証明アシスタント（例：Lean）のコストを大幅に削減し、数学やソフトウェア工学において主流となり、標準的な実践になるまでに至る。
陶哲轩は主に数学証明の形式化に焦点を当てているが、その見解はソフトウェア工学にも直接適用できる：AI が生成したコード + 証明により人工レビュー
証明アシスタント（インタラクティブ定理証明器とも呼ばれる）は、人間がコンピュータを用いて厳密に数学定理を証明したり、ソフトウェア/ハードウェアの正しさを検証したりするためのツールです。
| ツール | 特徴・ハイライト | 代表的なプロジェクト/実績 |
|---|---|---|
| Lean 4 | 高速、オートメーションが強力、コミュニティが活発、AI フレンドリー | Mathlib 最大の数学ライブラリ；IMO 銀メダル（AlphaProof） |
| Rocq/Coq | 歴史最長、コード生成が強力、小核が信頼性高い | CompCert コンパイラ、seL4 の初期検証 |
| Isabelle | 高階論理、ドキュメント生成が優秀、産業応用が多数 | seL4 完全検証、Archive of Formal Proofs |
| F* | プログラム検証とコード生成のために特化 | 安全クリティカルソフトウェア、暗号プロトコル |
| Agda | 依存型の純度が高く、理論研究に適す | |
| HOL Light/HOL4 | 極小核、数学証明に強い | ケプラー予想の証明 |
この GitHub リポジトリ は、陶哲轩が2025年5月31日に正式に開始したオープンソースプロジェクトで、彼の古典的実解析教材《Analysis I》（学部レベル）をLean 4証明支援ツールで形式的に翻訳することを目的としています。
sorry（プレースホルダー）で示され、読者が自分でリポジトリを fork して証明を埋めることが奨励されます。プロジェクトは非常に速く進んでおり、全書の主要内容（第1章の序論は未形式化）をほぼカバーしています：
Bartosz Naskręcki
数学者 | @UAM_Poznan 副学部長 | @ccaiwut 研究者 | 厳密な数学、プログラミング &ML | AI が本当に理解していることに情熱を持つ
例：この数学者は HarmonicMath を使って数学定理の形式的証明を加速させました。
数学論文は形式的検証が必要です。通常、このプロセスは査読者が非公式に行います。しかし、もしより信頼できる方法、例えば Lean 4 コードへの自動形式化に依存できれば、査読者の役割は定義や定理の記述を細かくチェックすることに簡素化されます。その場合、自動生成されたコードのコンパイル結果自体が証明書となります。これは私と @HarmonicMath の Aristotle が長期実行で実現した成果です。
@PietroMonticone と @llllvvuu にブループリント構築過程での支援に感謝します。ここで、私の友人 Stefan Barańczuk の Chebyshev 整除列（Chebyshev divisibility sequences）に関する論文の完全かつ正確な自動形式化成果を示します。このコードは約 5000 行の高度に非平凡な Lean コードを含み、元の論文の様々な不整合や欠陥を修正しただけでなく、元々省略されていた命題も証明しています。
関連成果はこちらで確認できます：
私はこのような実験をシリーズで順次公開し、初等数論、組合せ数学、解析（すなわち Mathlib がカバーするすべての内容）を含む特定の数学分野において、数学的証明の有効性を文書化する大規模な転換が近いことを示すつもりです。私は、この一年が非常に忙しいものになると考えています！
もし私が今日の学生で、最先端の大規模言語モデルと対話することが「チート」だと感じるなら、今朝黒板の写真を撮って ChatGPT‑5.2‑Pro に背景、解法、そして Chevalley の可構成集合（constructible sets）に関する有名な定理への補足コメントを説明させました。受け取ったのは、全インターネットからの高品質な代数幾何学資料を総合した、非常に深いレポートで、その簡潔さと深さに驚かされました。
これは重大な問題を提起します：現代の学生が直面している真の努力と挑戦とは何でしょうか？コストは確かに要因ですが、これらのモデルが利用可能になったら、情報が豊富な時代にどう学ぶべきか？この時代、説明、参考文献、インタラクティブな探索はほぼ即座に手に入ります。
おそらく、真の困難は情報の取得方法や孤立した議論の理解ではなく、判断力の育成にあります。どのような質問をすべきか、どの説明が信頼できるかを知り、深い洞察と表面的に妥当なものを区別し、考えを真に内面化することです。答えがすぐ手に入る環境では、真の挑戦は味覚や数学的直感を形成し、知識が急激に氾濫する中で航行する方法を学ぶことにあるでしょう—沈むのではなく。
@HarmonicMath 数学的超知能を構築
Harmonic は Robinhood の創業者兼 CEO の Vlad Tenev と Tudor Achim によって共同設立され、新型の人工知能システム——Mathematical Superintelligence（MSI、数学超知能）を開発することに取り組んでいます。その目標は、AI に人間のトップ数学者に匹敵またはそれを超える形式的推論と証明能力を備えさせることです。
このラボの代表的な成果は Aristotle という AI システムです。Aristotle は 2025 年の国際数学オリンピック（IMO）で歴史的な金メダルレベルのパフォーマンスを達成し、標準的な数学推論ベンチマーク（例：MiniF2F）で90% の正確率を記録しました。さらに注目すべきは、Aristotle が6 時間で数学界を 30 年悩ませてきた公開問題を解決したことで、強力な問題解決能力を示しました。
Harmonic は、真のインテリジェンスは答えだけに注目すべきではなく、推論過程の正確性に注目すべきだと強調しています。「答えが正しいかどうかを知りたいとき、私たちがチェックするのは推論—その論理的ステップです」。長期的なビジョンは、数学超知能を単なる研究ツールに留めず、広く公平に利用できるようにすることです。「数学超知能はすぐに到来し、均等に分配されるべきです」。
2025 年末までに、Harmonic は1 億米ドルの資金調達を受け、「ユニコーン」企業に昇格し、業界からその技術路線が高く評価されていることを示しています。
Harmonic の x アカウントは人工知能と数学分野の著名な学者から注目されています。
Chieh-Hsin (Jesse) Lai (@JC JesseLai)
chiehhshinjesselai.github.io でより詳細な研究成果が掲載されている可能性があります。Christian Szegedy (@ChrSzegedy)
Emily Riehl (@emilyriehl)
前提知識
離散数学の基礎を確実にマスターすること：命題論理、述語論理、帰納証明、集合論、関数。
ツール選択と証明アシスタント入門
CoqまたはLeanから始めることを推奨します（両方とも最も人気があり、コミュニティが活発です）。
学習パス：公式のインタラクティブチュートリアルに従ってステップバイステップで練習します。
進階
ETH Zurich の数学者 Johannes Schmitt は重要なマイルストーンを発表しました：OpenAI の GPT-5 モデルが初めて完全に自律で数学分野のオープン問題（open math problem）を解決し、完全かつ正しい証明を提供し、人間からの指示や介入は一切ありませんでした。
具体的な内容は、列挙幾何学（enumerative geometry）における小さくも新しい貢献に関するものです：曲線のモジュライ空間（moduli spaces of curves）上の交叉数（intersection numbers）を扱っています。著者は分野の専門家に相談し、この問題が未解決で明確な解法がないことを確認したうえで、彼が参加しているベンチマークプロジェクト IMProofBench（AI の数学証明能力をテストするプラットフォーム）に提出しました。
GPT-5 は優雅な証明を提示し、従来の複雑な理論を回避して、代数幾何学の別の分野から技術を借用し、「外部者の視点」の新しいアプローチを提供しました。
その後、彼らは共同で論文を執筆し、複数の AI モデルの貢献（GPT-5 と Gemini 3 Pro の証明、Claude の執筆支援、Lean 形式化検証）を統合し、各段落の AI／人間の出所を透明に示し、プロンプトログも添付しました。これは人‑AI 協働の新たな実験と見なされています。
興味深い結末として、GPT-5 は完璧な一般証明を提示した後、特定のケースの例示式で幻覚（hallucination、完全に作り上げた誤情報）を起こし、後に別の AI（Claude）によって指摘されました。
幻覚の例
総じて、この投稿は AI が高度な数学研究において「補助ツール」から「独立した発見者」へと重要な一歩を踏み出したことを示し、数学界と AI コミュニティの間で広範な議論を呼び起こしています。
問題の出所：Schmitt は IMProofBench というプロジェクトに参加しました。これは AI の 研究レベルの数学的証明 能力をテストするためのプライベートベンチマーク（データ汚染を防ぐため）で、複数の数学者が提出した PhD レベルのオープン問題を収集しています。
具体的な問題：安定曲線モジュライ空間 \\overline{\\mathcal{M}}_{g,n} 上の純粋 ψ クラス交差数（descendant integrals）：
ただし $\sum e_i = 3g-3+n$（次元制約）。
問題：固定された g,n に対して、どの指数ベクトル \mathbf{e} = (e_1, \dots, e_n) がこの交差数を 最大化 するか？
結果：最大値は balanced ベクトル（$e_i$ ができるだけ均等に分布し、隣接差が最大でも 1）で達成され、最小値は質量がほぼ一箇所に集中するベクトルで達成されます。
証明の概要：AI（GPT‑5）は、従来の理論（例：Witten‑Kontsevich 定理）を全く使わず、ψ クラスの抽象的な交差数性質である nefness（nef クラス）と Khovanskii‑Teissier 不等式（対数凹性）だけを用いて簡潔な証明を提示しました。
論文：Schmitt はすぐに論文を書き、arXiv（arXiv:2512.14575、タイトル『Extremal descendant integrals on moduli spaces of curves: An inequality discovered and proved in collaboration with AI』）に投稿しました。論文中では AI が執筆した部分を明示し、透明性を示すためにログも添付しています。
これはマイルストーンです：研究レベルのオープン数学問題を AI が単独で解決した既知の最初の公開事例となります（以前は AI はコンテスト問題や既知問題での活躍が中心でした）。
GPT‑5 がまず自然言語で証明を生成し（Schmitt と共同作業者が正しさを検証）ました。
他の AI（例：Gemini 3 Pro、Claude Opus 4.5）が論文本文の大段落執筆を支援しました。
GPT‑5.2 と Claude Code が Lean コードの生成を支援しました。
Schmitt 自身は Lean の経験が全くなく、1 日で AI の「vibe‑coding」（適当に生成＋反復）により形式化を完了しました。
証明は二つの部分に分かれています：
組合最適化部分（Theorem 3.1）：対称的な対数凹関数が balanced ベクトルで最大になることを示す純粋な組合不等式です。この部分は Lean で完全に形式化されており（約 3.5 ページの PDF）、コードは以下です。
原始 Lean コード：GitHub - schmittj/balanced-vectors-blueprint: Lean Blueprint for technical lemma on maxima and minimal of certain log-concave functions
幾何部分（Theorem 3.2）：descendant integrals が上記関数性質（nef + log‑concavity）を満たすことを証明します。この部分はまだ非形式的です。モジュライ空間自体が Lean/mathlib に未定義であり、これは大規模なプロジェクトで数年を要する可能性があります。
コミュニティメンバー Eric Vergo が コードを高速にリファクタリング し、mathlib スタイルに合わせ、AI 生成 Lean 証明テンプレートのテストケースとして利用できるようにしました。
Kim Morrison（Lean のエキスパート）が、定義と証明の分離や警告の追加（定義は人手でレビューが必要）といった改善提案を行っています。
形式化の利点：組合最適化部分は煩雑な不等式が多くミスが起きやすいですが、Lean による検証で 安心感 が得られます。Schmitt はこれが「検証効果の 50 %」を占めるが、作業量は「0.01 %」に過ぎないと評価しています（全体の代数幾何的背景を形式化するのとは比較できません）。
驚きと称賛：多くの人が AI がオープン問題を解決し、経験ゼロで Lean を形式化したことに驚嘆しています（「vibe‑formalizing」）。
Kevin Buzzard（Lean コミュニティのリーダー）は、モジュライ空間の定義自体が巨大な空白であり（楕円曲線のモジュライ空間すら Fermat の最終定理に対して未整備）、幾何部分の形式化には数年かかる可能性があると指摘しています。AI は定義の信頼性に欠けるが、小さな補題の補完には有用です。
形式化 AI 証明の規範：AI が生成したコードの信頼性問題への対処法が議論されています。
提案：定義は別ファイルに置き、大きな警告を付けて必ず人手でレビューする。
mathlib の断片化回避：優先的に主リポジトリへ統合する。
「quarantine」という、証明義務のない定義を一時的に隔離し、レビューしやすくする方策も検討されています。
より広い哲学的議論（Timothy Chow ら）：
mathlib は唯一の正典的定義源になるべきか？しかし数学概念はしばしば複数の等価定義（クラス A）や、等価でないが関連する取り決め（クラス B、例：Fourier 変換の正規化）を持ちます。
形式化は数学の「非形式的意味合い」を完全に捉えられるか？（例：可証明性の微妙な差異、Gödel の不完全性、数学者の「直感」）
Kevin Buzzard は、実際の論文で使われる定理（例：Sylow の定理）は基礎的な接続に依存しないことを指摘しています。
AI の数学研究における役割：この事例は、最先端 AI が新しい証明を発見し、従来のアプローチを回避し、形式化を支援できることを示しています。
将来のトレンド：人間＋AI のハイブリッド証明の規範が整備され、AI の貢献を扱う専用テンプレートが登場し、mathlib が代数幾何を徐々にカバーしていく可能性があります。
現在の状況（2025 年 12 月）：GPT‑5 は IMProofBench で最高のパフォーマンスを示し、22 % の問題を完全に正解しています。これにより、AI が研究レベルの数学支援においてすでに実用的な段階に達していることが分かります。
期待に満ちており、数学は形式的検証が必要です。しかし、今はまだ使いにくいと聞いています。
2025年12月8日 —— 著名な数学者でフィールズ賞受賞者のテレンス・タオ（Terence Tao）は、最近自身の個人ブログでエルデシュ問題#1026の完全な解決過程を詳述しました。この1975年に提起された古典的な未解決問題は、オンラインコミュニティの協力、人工知能ツール、既存の文献の組み合わせにより、最終的に2025年12月に完全に解決されました。
Erdős 問題#1026 は、ポール・エルデシュ（Paul Erdős）が単調部分列について研究したことに由来します。この問題は当初、やや曖昧に表現されていました：与えられた distinct な実数列 a_1 < a_2 < \dots < a_n に対し、最大単調部分列の和の上限を求める。コミュニティによる明確化と再定式化を経て、この問題は定数 c_k の正確な漸近挙動を決定することと同等であることが分かりました。ここで c_k は、総和が 1 に正規化された列において、Bob（単調部分列を選択する側）が保証できる最大のシェアを表し、Alice はそのシェアを最小化しようとします。最終的な証明は、c_k = 2 / \sqrt{k} が上限であり、k が完全平方数のときに厳密に達成されることを示しています。
解決プロセスは2025年9月12日に始まり、この問題は正式にエルデシュ問題サイトに
その他の資料