2026年10月9日、数学者テレンス・タオ（Terence Tao）がカリフォルニア工科大学（Caltech）で「Math 2.0」と題する公開講演を行いました。講演資料は翌10日、タオ本人のブログで公開されています。
タオが「Math 2.0」と呼んでいるのは、AIによって数学の証明が豊富になる時代に合わせて、研究の進め方を再構成するという構想です。AIを使って数学研究の最前線を広げると同時に、問題解決が中心だった研究のあり方を見直し、人間の数学的理解を強化することを目指しています。
AIが数学の難問を解くようになり、以前は難しいと考えられていた問題にも、比較的短時間で解答が得られる例が出ています。証明をコンピューターで検証するソフトウェア（証明支援システム）のLeanなどを使えば、専用の形式で書かれた証明を機械的に検査できます。
こうした変化の中で、タオは次の問題を提起しました。
数学の問題を解決することは、数学を発展させるという長期的な目的の代理指標にすぎないというものです。
タオは講演スライド（PDF）の9ページで、証明が希少だった時代には、この指標がおおむね機能していたものの、証明が豊富になる時代には、本来の目的との間にずれが生じていると述べています。
問題解決だけを盲目的に最適化し続けることは、数学の長期的な発展に害を及ぼすとも警告しています。
Math 1.0からMath 2.0へ 証明が希少だった数学の変化
タオは従来の数学研究を「Math 1.0」と呼び、その特徴を「証明の希少性（Proof Scarcity）」にあると説明しています。
数学の未解決問題に正しい解答を与えることは難しく、多くの場合、専門家の高度な知識が必要でした。
数学界の制度や伝統、研究者への動機づけ、研究目的の多くも、証明が希少であることを前提に形成されてきたとタオは述べています。
AIの数学能力が向上したことで、この前提が変わり始めました。
数学がAIと相性のよい理由
タオは、数学には現代のAIが能力を伸ばしやすい三つの条件がそろっていると説明しています。
第一に、数学の証明は客観的に検証できます。
数学者同士でも、どの研究が面白いか、将来どの分野が発展するかについて意見が分かれることはあります。一方、与えられた問題に対する証明が論理的に正しいかどうかには、共通の判断基準があります。
さらに、Lean（リーン）などの証明支援システムを使えば、専用の形式で記述された証明をコンピューターで検証できます。
Leanは、数学の定義や定理、証明を形式的な言語で記述し、論理的に正しいかを確認する仕組みです。AIが生成した証明も、Leanで扱える形式にすれば、与えられた定義や前提から結論が導かれるかを機械的に検査できます。
第二に、数学の証明はデジタル化しやすいことです。
純粋数学（現実への応用を直接の目的とせず、数学そのものを研究する分野）の証明を作成したり検証したりする際、物理的な実験装置や現実世界からの測定データは必須ではありません。必要な定義や既存の定理がそろっていれば、紙と鉛筆、あるいはコンピューター上で研究を進められます。
第三に、数学には質の高い研究資料が大量に存在しています。
数学の難問を解くには、過去の研究成果や専門的な文献が必要になる場合があります。膨大な数学論文や教科書がデジタル化されていることも、AIによる研究を支える条件の一つです。
タオは、客観的な検証可能性、デジタル化の容易さ、質の高いデータという三つの特徴が、数学を機械学習（データからコンピューターが規則を学ぶ技術）に適した分野にしていると説明しています。
こうした条件とAI開発への大規模な投資が重なり、数学は「証明の豊富さ（Proof Abundance）」を特徴とする時代に入りつつあります。
AIの数学能力には大きなばらつきがある
AIの数学能力は、問題の種類によって大きく異なります。
タオは現在のAIの能力を、得意な作業と苦手な作業の差が大きい「Jagged Capability」（ギザギザした能力）と表現しています。
十分な計算資源（計算に使うコンピューターの性能と時間）と高性能なAIモデルを利用すると、以前は難しいと考えられていた多くの未解決問題に、比較的短時間で解答を得られるようになりました。
一方、数学研究の最前線にある問題の大半は、依然として未解決です。
AI開発企業の発表やSNSでは成功例が注目されやすい一方、失敗した試行が同じように報告されるとは限りません。
例えば、仮にAIが100件の問題に挑戦して1件を解決した場合と、2件に挑戦して1件を解決した場合では、同じ1件の成功でも評価の意味が異なります。これは説明用の仮の例です。
タオは、成功例だけでなく、失敗例や使用した計算資源も含めた透明性の高い評価が必要だと指摘しています。
その試みの一つが、First Proofです。First Proofは、AIが研究水準の数学問題について、どの程度の証明能力を持つのかを調べる取り組みです。個別の成功例だけで性能を判断するのではなく、具体的な課題を用いて能力を評価する方向性を示しています。
数学の問題を解くだけでは、なぜ不十分なのか
代理指標の意味は、テストの点数にたとえると分かります（記事側のたとえ）。
学習の目的は知識を身につけることですが、その成果を確かめるためにテストの点数を使うことがあります。点数が理解度を反映している間は役立ちますが、点数を上げることだけに集中すると、学習の目的から外れる場合があります。
未解決問題は目的地ではなく「灯台」
タオは、数学における未解決問題の役割を「灯台」にたとえています。
灯台は、進む方向を知るための目印です。そこへ到達することだけが目的ではなく、灯台を目指して周囲を探索することにも意味があります。
数学の未解決問題も、研究者がどの方向を調べればよいかを示す役割を持ちます。
最終的に問題を解けなかった場合でも、その過程で得られた知見が価値を持つことがあると、タオは述べています。成功、失敗、部分的な進展のいずれからも、研究に役立つ教訓が得られる場合があります。
AIが灯台へ早く到達しすぎると、そこへ向かう途中で探索されるはずだった別の道が調べられなくなる可能性があります。
タオが懸念しているのは、こうした探索機会の減少が数学の発展に与える影響です。
人間の理解が数学研究を循環させる
タオは講演スライドの17〜19ページで、数学研究の仕組みを図にしています。
最も単純な図では、数学の問題から解答が生まれます。そこにAIを加えると、問題解決の流れを強化することが考えられます。
一方、タオが示した別の図には「人間の理解」が加わっています。
タオの図では、純粋数学の問題を解く過程で得られた洞察が「人間の理解」となり、応用数学にも安全に引き継がれる「再生可能な循環（renewable cycle）」として描かれています。
タオは続く19ページで、AIを無差別に使い、この再生可能な循環を維持しない形で問題を解き続けると、数学という分野の長期的な健全さと進歩が損なわれ、現実の応用への安全な橋渡しにも悪影響が及ぶと述べています。
大量の問題をまとめて調べる「実験数学」
タオは、これまで現実的でなかった規模の数学的なデータを集められるようになり、新しい「実験数学」が可能になったと説明しています。
個別の問題を詳しく調べる研究に加えて、多数の関連する問題をまとめて調べ、全体の傾向を把握する研究も現実的になっています。
タオはこの違いを、個別事例の研究（case studies）と集団調査（population surveys）という言葉で表現しています。
その具体例が、Equational Theories Project（ETP）と、逆ガロア問題を扱う競技IGP24です。
2,200万件の関係を判定したEquational Theories Project
2024年から2025年にかけて行われた「Equational Theories Project（ETP）」では、人間の研究者と自動化された証明手法を組み合わせ、22,028,942件の数学的な関係を調べました。
対象となったのは、普遍代数学（さまざまな代数的構造に共通する性質を研究する分野）の「マグマ（magma）」です。
マグマは、ある集合と、その集合に属する二つの要素から一つの要素を得る演算を持つ数学的な構造です。演算の結果が同じ集合に属すること以外に、交換法則や結合法則などの規則は要求されません。
ETPでは、マグマの演算を最大4回使って表せる4,694種類の等式法則について、ある法則から別の法則が導かれるかを調べました。
等式法則とは、演算を使った等式で表す規則のことで、例えば、演算の順序を入れ替えても結果が同じになるという交換法則 x ⋄ y = y ⋄ x がその一つです。
一つの法則から、自分自身を除く4,693種類の法則への関係を考えるため、関係の数は次のとおりです。
4,694 × 4,693 = 22,028,942
この数字は独立した未解決難問の数ではなく、4,694種類の法則の間にある関係の数を表しています。
ある法則から別の法則が導かれる場合は証明を作り、導かれない場合は、最初の法則は成り立つのに次の法則は成り立たないマグマを見つけて反例とすることで、判定を進めました。
2024年10月12日にタオが公開した途中経過では、開始から19日間で全体の99.9963％が判定され、826件が未解決として残っていました。
その後も共同研究が続き、2025年4月14日に22,028,942件すべての関係について判定が完了しました。
2,200万件を判定した方法
成り立つ関係の判定では、従来型の自動定理証明器（Automated Theorem Prover、ATP）が主要な手段の一つとして使われました。
自動定理証明器は、与えられた条件から結論を導く証明を、決められた論理規則に従って探索するプログラムです。
成り立たない関係の判定では、要素の数が有限の小さなマグマを総当たりで調べる方法や、演算を ax + by の形で与える線形モデルなどによる反例の構成が使われました。
2024年10月の途中経過でタオは、中核となる含意（ある法則から別の法則が導かれること）の判定では、従来型の自動定理証明器のほうが現代のAIツールより優れていたと報告しています。
当時、大規模言語モデルは、Leanの証明やソフトウェアのコードを書く補助、可視化ツールの開発などに使われていました。
ETPの2,200万件の判定は、人間の研究者、従来型の自動定理証明器、形式的な検証システムを組み合わせた共同研究の成果です。
Leanでは、成り立つ関係10,657件と成り立たない関係586,925件の合計約60万件を、Leanで検証できる形に記述しました。
残りの関係は、これらの結果をもとに、推移律と双対性を利用するLean外部のプログラムによって導いています。
推移律は、法則Aから法則Bが導かれ、さらに法則Bから法則Cが導かれるなら、法則Aから法則Cも導かれるという性質です。双対性は、マグマの演算の左右を入れ替えた法則どうしにも、元の法則どうしに対応する関係が成り立つという性質です。
論文によると、この過程で、特定の等式法則を満たす新しいマグマの構成方法が見つかりました。
有限のマグマに限った場合の関係も調べられ、双対の関係と合わせた2件を除いて判定されました。
この成果は、2025年12月に公開された研究プレプリント（査読前に公開される論文）で報告されています。
25,000種類の群を調べる逆ガロア問題への挑戦
タオが紹介したもう一つの事例が、2026年の「Inverse Galois Problem Challenge（IGP24）」です。
逆ガロア問題は、数学的な対称性を表す「群」を指定したとき、その群をガロア群として持つ多項式が存在するかを問う問題です。
多項式とは、例えば x² + 3x + 2 のように、変数のべき乗を組み合わせた式です。次数は変数の最も高い指数で、この式は2次です。
ガロア群は、多項式の解が持つ対称性を数学的に表したものです。例えば、解を入れ替える操作のうち、解同士の数学的な関係を保つ操作を調べます。
逆ガロア問題では、先に群を与えて、それに対応する多項式を探します。
IGP24では、次数24の多項式に対応する25,000種類の推移的な群を対象に、具体的な多項式を探索しました。
ここでいう推移的とは、群に含まれる操作を適切に組み合わせることで、24個の対象（多項式の解）のどれからでも、別の対象へ移せる性質のことです。
競技では、最高次の係数が1である整数係数の24次多項式を提出し、対応するガロア群と実数の解の個数を検証します。提出する多項式には、有理数を係数とする多項式に分解できない「既約」という条件もあります。
群の種類（25,000）と実数の解の個数を組み合わせた評価対象は、165,836件です。
提出された多項式は、数学ソフトウェアで条件を満たしているかが検証されます。
タオはIGP24の共同主催者の一人で、講演では次数24を対象にした第一段階を成功した共同探索として紹介しています。また、第二段階では次数31まで対象を広げる計画を示しています。
IGP24の公式リポジトリには、競技のルールや提出形式、検証ツールなどが公開されています。
この取り組みは、対象を具体的な次数に限定した探索です。有理数を係数とする多項式で、すべての有限群をガロア群として実現できるかという一般的な逆ガロア問題は、現在も未解決です。
大量の問題を調べることで分かること
ETPとIGP24は、数学的な研究対象が異なります。
ETPでは、ある法則から別の法則が導かれるかという関係の真偽を判定しました。一方、IGP24では、指定された群を実現する具体的な多項式を探索しました。
記事側の整理として、両者に共通しているのは、大量の関連する問題をまとめて扱い、その結果を検証・蓄積する研究方法です。
タオは、大規模な数学データを使うことで、AIが使える時代の新しい「難しさの地形（Difficulty Landscape）」を調べられると述べています。どの種類の問題が難しく、どの種類の問題が解きやすいのかという分布を、これまでとは異なる規模で研究できる可能性があります。
これは今後の研究の方向性で、難易度分布の全体像はまだ明らかになっていません。ETPやIGP24は研究対象を大きく広げた実例で、その結果を数学的な理解につなげる活動も、Math 2.0に含まれます。
Math 2.0はAIをどう使うのか
人間の理解が数学と関わるさまざまな場面でAIを活用するというのが、タオの示す方向性です。
タオは講演スライドの23ページで、より持続可能なAIの使い方を図に示しています。
従来の数学研究を説明する図には、純粋数学の問題と解答、応用数学（現実の問題を数学で扱う分野）の問題と解答、そして人間の理解が登場します。
Math 2.0の図では、問題から解答を得る部分だけでなく、人間の理解と数学が結びつく複数の部分に「+AI」が追加されています。
純粋数学では、証明が正しいかどうかを客観的に検証できます。一方、現実世界に数学を応用する場合には、得られた解答が人間の目的に合っているかという判断も必要になります。
すでに証明された定理を、もっと分かりやすくする
数学には、すでに正しいことが証明されていても、その証明を理解するのが難しい定理があります。
既知の証明が不透明で、なぜその証明が成り立つのか、その考え方や動機が見えにくい場合です。
タオは、こうした問題を「Open Exposition Problems」と呼び、未解決の研究問題とは区別しています。
ここでの目的は、すでに得られた数学的な成果を、より納得しやすい形で説明することです。
例えば、ある定理について二つの証明があったとします（記事側の例）。一つは多くの高度な理論を使った長い証明で、もう一つは少ない前提で同じ結論を導ける証明です。
後者が見つかれば、その定理が成立する理由を別の角度から理解できる可能性があります。新しい証明方法は、別の問題にも応用できるかもしれません。
ここで得られる価値は、証明された定理の数では測れません。同じ定理について、理解の仕方が増えることに意味があります。
タオが紹介している「Caltech Mathathon」は、そのような研究を試みるイベントです。
Caltech Mathathonで既存の証明を改善する
2026年11月13〜15日、カリフォルニア工科大学の学生が主催する「Caltech Mathathon」が開かれる予定です。
大学の公式案内では、AIを使って人間の数学的理解をどう強化できるかという問いを中心に据えています。
タオの講演資料によると、参加者はオープンソース（設計やコードが公開され、誰でも利用できる形で提供されるもの）のAIツールを使い、既存の数学的成果に対する新しい証明や、改善された証明を探します。
対象は、現在知られている証明に何らかの不満が残っている問題です。例えば、証明の一部を別の方法で説明できないか、もっと少ない前提で証明できないかという方向が考えられます。
2026年10月12日時点では開催前で、成果はまだ出ていません。
数学の知識を更新可能なネットワークにする
数学の研究成果は、多数の論文や専門書に分散しています。
ある定理が別の論文にある結果を前提としていたり、同じ理論が複数の分野で異なる形で使われていたりします。
研究者は、こうした関係を理解するために多くの文献を調べなければなりません。
タオはMath 2.0の具体例として、複数の研究論文を統合し、更新し続けられる知識ネットワークにまとめることを提案しています。
IEANTNという数学の知識ネットワーク
その初期的な取り組みが「Integrated Explicit Analytic Number Theory Network（IEANTN）」です。
これは、明示的な解析的整数論の研究結果を統合するネットワークです。
解析的整数論は、素数などの整数の性質を、解析学の手法を用いて研究する分野です。
名称の「Explicit（明示的）」は、数値の評価や定数を具体的に示すことを指します。例えば、ある誤差が「十分小さい」と分かるだけでなく、具体的にどの程度以下かという評価を扱います。
こうした研究では、多数の定理や評価式が互いに関係しています。ある定理の評価が改善されると、それを利用する別の結果にも影響が及ぶ可能性があります。
タオは、このネットワークを生きた表計算シートにたとえています。新しい研究成果はネットワークに追加でき、結果を取り除いたときも、関連する部分を更新できます。
論文を読むことから、知識の関係を調べることへ
数学の論文は、ある時点で得られた研究成果を記録する形式です。
研究が進んで新しい証明や改善された評価が見つかっても、過去の論文そのものが自動的に書き換わるわけではありません。
知識ネットワークでは、個々の研究成果に加えて、その成果がどの定理に依存し、どの結果に利用されているのかという関係を管理できます。
例えば、ある評価式を改善したとき、その式を利用している別の定理も改善できるかを調べやすくなる可能性があります。
このように個々の定理を別々に扱うだけでなく、数学的な知識がどのような関係で成り立っているのかを調べられることは、人間の理解を強化することにもつながる可能性があります。
LeanとMathlibで数学を形式化する
タオは、大規模で質の高い形式数学ライブラリを作ることも、Math 2.0の具体例として挙げています。数学の証明を、コンピューターが検証できる形式的な言語で書き直すことを、形式化といいます。
その代表的な存在がMathlibです。
Mathlibは、Leanで利用できる数学の定義、定理、証明などを集めたライブラリです。
数学の論文に書かれた通常の証明を、Leanで検証できる形式に変換するには作業が必要です。人間の数学者にとって自然な省略や、暗黙の前提が、コンピューターにはそのままでは伝わらないためです。
AIを利用して形式化された数学の知識を増やせれば、研究者はより多くの既存の定理を再利用できるようになります。
新しい原理や方法を見つけるAIの使い方
タオは、Math 2.0におけるAIの使い方として、新しい証明を見つけることに加え、新しい原理、方法、洞察を見つけることを挙げています。
講演スライドの27ページでは、さらに具体的な例として、「アブレーション研究」と、定理の周辺を自動的に探索する方法を挙げています。
証明に使われた理論を取り除いてみる
アブレーション（Ablation）とは、ある仕組みの一部を取り除き、その部分がどのような役割を果たしているのかを調べる方法です。
タオは、数学でも同じ考え方で、すでに証明された定理から、証明に使われた主要な理論や入力を取り除いても証明できるかを調べる方法を挙げています。
例えば、高度な数学理論を使って証明された定理について、その理論を使わずに、もっと初等的（基本的な理論だけを使う）な方法で同じ結論を示せないかを探索します。
別の証明が見つかれば、元の定理が成立する理由について新しい理解が得られる可能性があります。
また、ある理論を取り除くと証明できなくなることが分かれば、その理論が証明の中で担っている役割を検討する材料になります。
定理の成立条件を変えてみる
もう一つは、定理の成立条件を変更したとき、どの結論が残るかを調べる方法です。
数学の定理には、結論が成立するための条件が定められています。
例えば、ある定理が「条件Aと条件Bを満たすとき、結論Cが成り立つ」という形だったとします（記事側の例）。このとき、条件Bを取り除いても結論Cが成立するのかを調べられます。
結論Cが成立しなくても、その一部分にあたる結論Dなら成立するかもしれません。
こうした探索を繰り返すと、元の定理がどの条件に依存しているのか、どの範囲まで一般化できるのかが分かってきます。
タオはこれを、定理の周辺を自動的に探索する方法として紹介しています。条件を体系的に変えることで、新しい問題や法則が見つかる可能性があります。
数学専用のオープンソースAIモデルという構想
タオは、数学の作業に特化したオープンソースAIモデルの開発にも言及しています。
講演で示された方向性は、数学的な作業を効率的に実行でき、解釈可能性（Interpretability）と安全性（Safety）を重視したモデルを作ることです。
解釈可能性は、AIの内部でどのような処理が行われ、結果がどのように生まれるのかを人間が調べ、理解できる性質に関係しています。
タオは講演で、一部のオープンな数学モデルが近く公開される予定であることにも触れています。講演資料には、具体的なモデル名や性能、公開後の利用条件は示されていません。
数学の研究成果をインタラクティブな教材にする
タオは、数多くの研究結果を統合し、読者が操作しながら読める形に整理した数学の教材やプレゼンテーションを作ることも提案しています。
数学の専門書や論文では、ある理論を理解するために多数の前提知識が必要になることがあります。
また、同じ理論について異なる研究者が別の視点から説明している場合もあります。
AIを使えば、複数の研究成果の関係を整理し、理解する順序に沿って説明を構成することが考えられます。
例えば、ある定理を理解するために必要な定義や補題を順番に提示したり、具体例を変更したときに結論がどう変わるかを調べられる教材が考えられます。
既存の研究成果を理解しやすい形に再構成できれば、数学者は過去の知識を研究に利用しやすくなります。
数学的に正しいAIの答えは、現実でも適切なのか
数学的に正しい答えが、現実の目的にも適切だとは限りません。
証明が示すのは、設定された前提から結論が論理的に導かれることで、その前提が現実の状況を十分に表しているかどうかは、証明の内部だけでは判断できないからです。
タオはこの違いを説明するため、講演スライドの20〜21ページで架空のがん治療を使った思考実験を提示しています。
AIががん治療法を発見するという思考実験
高性能なAIに、がんの治療法を見つけるよう指示したとします。
指示には、第III相臨床試験（新しい治療法の効果と安全性を、多数の患者で確かめる段階の試験）を通過することと、間違いを起こさないことも含まれています。
AIは大量の計算を行い、それまで知られていなかった化学物質の組み合わせを提案しました。
その物質を混ぜて患者に注射すると、がん細胞をすべて死滅させられるとAIは主張します。
人間には、AIがどのようにしてその組み合わせを発見したのか分かりません。
しかし、AIは何らかの方法で予測に対するLeanの証明書（Leanで検証できる形の証明）を提示し、治療法は第III相臨床試験にも合格したと仮定します。
ここまで条件がそろっても、タオはAIの解答が人間の目的とずれている可能性を問いかけています。
例えば、臨床試験の評価方法や、数理モデル（現実の現象を数式で表したもの）が現実を十分に表していない部分に弱点があった場合です。AIがそうした弱点を利用して条件だけを満たす結果を得ている可能性も考えられます。
人間が仕組みを理解することの意味
タオは続けて、患者自身がその治療を受ける状況を想定します。
自分が早期のがんと診断され、チャットボットから新しい治療法を勧められたとします。
少なくとも一人のがん治療の専門医が、その治療の作用機序（薬が体の中でどのように効くかの仕組み）を、部分的にでも理解していたら、患者は安心できるでしょうか。
あるいは、AIが使った数学的なモデルを理解している数学者がいたらどうでしょうか。
タオは、この問いを使って、人間の理解が現実世界の判断にどのような意味を持つのかを考えさせています。
純粋数学の理解を現実への応用に生かす
タオは講演スライドの28ページで、純粋数学のモデルを理解することで得られた知識や洞察を、現実世界での数理モデルの失敗を分析するために使うことを提案しています。
また、AIを応用数学に利用する際、人間の目的とAIの出力の間にずれがないかを調べることも挙げています。
人間がモデルを理解していれば、AIの解答にどのような前提があり、どこに適用上の限界があるのかを検討する材料になる可能性があります。
タオは同じ28ページで、Math 2.0の実現を妨げる最大の制約は、技術でも制度的な文化でもなく「想像力（Imagination）」だと述べています。
FAQ
Math 2.0とは何ですか？
数学者テレンス・タオが、AIによって数学の証明が豊富になる時代の研究のあり方を表現した言葉です。AIを使って数学研究の最前線を広げると同時に、問題解決が中心だった研究のあり方を見直し、人間の数学的理解を強化する構想です。
AIは数学の未解決問題をすべて解けるようになったのですか？
以前は難しいと考えられていた多くの未解決問題で、AIによる解決例があります。一方、数学研究の最前線にある問題の大半は未解決であり、AIの能力には問題の種類によって大きなばらつきがあります。
Leanで検証された証明なら必ず正しいのですか？
Leanが検証するのは、与えられた定義や前提から結論が論理的に導かれるかどうかです。現実世界への応用では、数理モデルの前提が適切かどうかも別に確認する必要があります。
Equational Theories Projectは何を達成した研究ですか？
一般のマグマについて、4,694種類の等式法則の間にある22,028,942件の関係の真偽の判定をすべて完了した研究です。2025年4月14日に主要目標を達成しました。
Equational Theories ProjectはAIが解いた研究ですか？
人間の研究者、従来型の自動定理証明器、Leanなどを組み合わせた共同研究です。2024年10月の途中経過でタオは、中核となる判定では従来型の自動定理証明器のほうが現代のAIツールより優れていたと報告しています。
IGP24では何を調べたのですか？
次数24の多項式に対応する25,000種類の推移的な群について、条件を満たす具体的な多項式を探索した競技です。群の種類に加えて実数の解の個数も区別するため、評価対象となる組み合わせは165,836件あります。
Math 2.0ではAIをどのような研究に利用しますか？
既存の証明の改善、数学の知識ネットワークの構築、形式的な数学ライブラリの拡充、定理の成立条件の探索などが挙げられています。数学の問題を解くことに加え、人間の理解を強化するための利用方法が提案されています。
参考・参照元
- Terence Tao — Math 2.0（2026年10月10日、本人によるブログ）
- Terence Tao — Math 2.0（2026年10月、講演スライド・PDF29ページ）
- Terence Tao — The Equational Theories Project: a brief tour（2024年10月12日）
- The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale（arXiv、2025年12月）
- Equational Theories Project — GitHub
- IGP24 — 公式GitHubリポジトリ
- First Proof — 公式サイト
- Caltech Mathathon Challenge — California Institute of Technology
- Mathlib — 形式数学ライブラリ
