Concise Summary简洁概述
Tao argues that formal verification, not AI, is the actual catalyst reshaping mathematics — it dissolves the trust problem that has always blocked large-scale math collaboration.
His Equational Theories Project proved this at scale: 50 mostly-unknown collaborators solved 22 million algebra problems in three months via Lean-verified, GitHub/Zulip-coordinated workflows — versus ~20 problems in prior comparable efforts.
陶哲轩指出，真正撬动数学工作方式的不是 AI，而是形式验证——它消解了长期阻碍大规模数学协作的信任难题。
他主导的等式理论项目证明了这一点：50 名彼此陌生的协作者借助 Lean 验证、GitHub/Zulip 协作，三个月解决 2200 万道代数题，而此前同类项目最多只处理过约 20 个。
Infographic信息图
Formal verification breaks the trust barrier
形式验证打破信任壁垒
Math collaboration used to require either line-by-line peer checking or trusting a contributor's reputation. A Lean-verified pipeline replaces both: anyone, known or anonymous, can submit, because the machine — not the community — certifies correctness.
过去数学协作要么逐行审查，要么靠声誉信任贡献者。有了 Lean 自动验证后，无论是否知名、是否露过面，任何人都能提交贡献，因为判定对错的是机器而非社群共识。
Modularity turned 22M problems into a GitHub-style project
模块化让 2200 万题变成了一个 GitHub 式项目
The Equational Theories Project split naturally into atomic sub-tasks — writing human proofs, translating to Lean, batch-solving 100k problems at once — so contributors needed only local context, not the whole picture, mirroring modern open-source workflows.
等式理论项目天然拆分成原子级子任务：写人类证明、翻译成 Lean、一次批量攻克 10 万道题——贡献者只需理解局部任务而非全局，与现代开源协作模式高度一致。
A single shared metric drove self-organizing progress
一个共享指标驱动了自组织式推进
By day 16, only 888 of 22 million implications remained unresolved. That single visible number became the target everyone pushed against, without central coordination — a mechanism closer to open-source issue trackers than traditional math collaboration.
项目第 16 天时，2200 万个蕴含关系只剩 888 个未解决。这个可见的单一数字成了所有人自发推进的目标，全程没有中心化协调——这种机制更像开源问题追踪器，而非传统数学协作模式。
Enlarge the pie, don't compete for it
把蛋糕做大，而不是抢蛋糕
Tao reframes AI's role: not replacing mathematicians on the hardest frontier problems, but clearing the long tail of medium-difficulty problems humans lack the manpower to attempt — making previously uneconomic mathematical goals newly feasible.
陶哲轩重新定义了 AI 的角色：不是在最难的前沿问题上替代数学家，而是清扫人类没精力覆盖的中等难度问题长尾——让此前经济上不划算的数学目标变得可行。
Detailed Summary详细解读
Tao opens by establishing math's extreme conservatism: an 1826 Cauchy textbook is still usable today, mathematicians are the last academics using chalkboards, and average co-authorship has crept from 1.5 to 2.5 while other sciences explode into mass collaboration. This sets up the puzzle the rest of the talk resolves — why has math resisted the scaling that transformed biology, physics, and citizen science?
He identifies three structural reasons: a doctoral-level entry barrier, zero fault tolerance (one wrong contribution among 100 destroys an entire proof), and a workflow — two or three people at a blackboard — that simply doesn't scale to internet-scale collaboration. These aren't cultural quirks; they're load-bearing constraints that any new collaboration model must actually solve, not paper over.
The pivot is formal verification: a Lean-based system that mechanically checks whether a proof step is valid. This directly neutralizes the zero-fault-tolerance problem — you no longer need to trust each contributor, only the verifier. It's the missing piece that makes anonymous, unvetted contributions safe to accept at scale, which is precisely what closed off mass collaboration before.
The Equational Theories Project is the proof of concept: 50 collaborators, mostly strangers to each other and to Tao, mostly non-professional mathematicians, generated and resolved 22,028,942 pairwise implications among 4,694 magma identities in three months on GitHub and Zulip — versus roughly 20 problems handled by prior comparable efforts. Success factors: modularity (tasks split into human-proof writing, Lean translation, batch-solving), a single visible shared metric (888 unresolved cases by day 16) that drove self-organized effort, and verification-enabled atomic-level technical debate — pinpointing exactly which of nine proof steps failed.
Tao then turns to LLMs directly, noting they solve olympiad problems yet flub basic arithmetic — and every mathematician who's tried them concludes unreliability is disqualifying on its own. His fix mirrors the verification logic above: pair an unreliable LLM with a verifier in a generate-check-feedback-correct loop. He cites AlphaEvolve (LLM plus genetic algorithm) breaking human records on finite-dimensional packing problems, while teasing unpublished progress on infinite-dimensional optimization.
The talk closes on a reframing: AI's biggest math contribution isn't beating humans on the hardest problems, but clearing a long tail of medium-difficulty problems no mathematician has time for — letting AI handle the easy fraction and escalate only genuinely hard cases to humans. This is explicitly "enlarge the pie, don't compete for it," and Tao caveats that every application is context-dependent, not plug-and-play.
陶哲轩开篇先建立数学极度保守的形象：1826 年 Cauchy 的教材今天仍可使用，数学家是最后还在用黑板粉笔的学术群体，论文平均作者数只从 1.5 缓慢爬到 2.5，而其他学科早已迎来协作规模的爆炸式增长。这个反差为全篇设下了要解决的谜题——为什么数学始终没能像生物学、物理学、公民科学那样实现协作规模化？
他归纳出三个结构性原因：门槛太高（通常需要博士学位才能理解问题本身）、容错率为零（100 份贡献里 1 份错误就能毁掉整个证明）、以及黑板前两三人讨论的工作流本身无法扩展到互联网规模的协作。这些并非文化怪癖，而是任何新协作模式都必须真正解决、而非绕开的硬约束。
关键转折是形式验证：一个基于 Lean 的系统能机械化判定一步证明是否成立。这直接化解了容错率为零的难题——你不再需要信任每一位贡献者，只需要信任验证器本身。这正是让匿名、未经审核的贡献也能被安全接纳的缺失环节，而这恰恰是此前阻断大规模协作的核心原因。
等式理论项目是这套逻辑的实证：50 名协作者——彼此大多素不相识，也多非专业数学家——在 GitHub 和 Zulip 上三个月内生成并解决了 4694 个 magma 恒等式之间的 2202.8942 万个两两蕴含关系，而此前同类项目最多只处理过约 20 个问题。成功要素包括：模块化分工（人类证明撰写、Lean 翻译、批量攻克互相独立）、一个可见的共享指标（第 16 天时剩 888 个未解决）驱动自发推进、以及验证机制让技术讨论精确到证明的某一原子步骤——比如九步证明中第九步报错时能精准定位问题。
陶哲轩接着直接谈及大语言模型：它们能解奥赛题，却连基础算术都会算错——每个尝试过的数学家最终都得出结论，这种不可靠性本身就是致命问题。他给出的解法呼应了前面的验证逻辑：把不可靠的 LLM 和验证器结合成“生成→检验→反馈→纠正”的循环。他举了 AlphaEvolve（LLM 加遗传算法）在有限维堆叠问题上打破人类记录的例子，并透露无穷维优化上也有尚未发表的新进展。
演讲收尾提出一个重新定义：AI 对数学最大的贡献不是在最难的问题上战胜人类，而是清理数学家没精力顾及的中等难度问题长尾——让 AI 先处理简单的部分，只把真正困难的案例上报给人类。他明确称之为“把蛋糕做大，而非抢蛋糕”，并特别提醒每种应用都高度依赖具体场景，并非即插即用。
FAQ常见问答
Isn't this just AI solving math, dressed up differently?这不就是 AI 解数学题的另一种说法吗？
No — Tao is explicit that the Equational Theories Project's core enabler was formal verification (Lean) plus mundane tools (GitHub, Zulip), not AI. AI/LLMs are discussed separately, and only become useful in math when paired with a verifier.
不是——陶哲轩明确指出，等式理论项目的核心推动力是形式验证（Lean）加上 GitHub、Zulip 这类平凡的协作工具，而非 AI。LLM 是单独讨论的，且只有配合验证器才能在数学中发挥作用。
Why can't you just crowdsource proofs without formal verification?为什么不能在没有形式验证的情况下直接众包证明？
Because math has zero fault tolerance: one wrong contribution among 100 invalidates an entire proof, and manually vetting every anonymous contributor doesn't scale. Formal verification replaces trust-in-people with trust-in-a-checker.
因为数学容错率为零：100 份贡献里只要有 1 份错误就会毁掉整个证明，而人工逐一审核每个匿名贡献者又无法规模化。形式验证把“信任人”换成了“信任检查器”。
How representative is one project of mathematics as a whole?一个项目能代表整个数学领域吗？
Not very — the Equational Theories Project is a narrow, highly decomposable algebra domain (magma identities) well-suited to automation. Tao doesn't claim this generalizes cleanly to, say, algebraic geometry or number theory research.
代表性有限——等式理论项目属于高度可拆解的代数子领域（magma 恒等式），特别适合自动化处理。陶哲轩本人也没有断言这能顺利推广到代数几何或数论研究等领域。
Does this mean LLMs are now reliable for math?这是否意味着 LLM 在数学上已经可靠了？
No — Tao explicitly states every mathematician who's tried LLMs concludes unreliability is disqualifying, citing a simple arithmetic error as an example. The fix is architectural (pairing with verifiers), not a claim that LLMs improved.
不是——陶哲轩明确说每个尝试过 LLM 的数学家都得出结论，其不可靠性是致命问题，并举了简单算术出错的例子。解法是架构层面的（配合验证器），而非声称 LLM 本身变得更可靠了。
What's the actual bottleneck this unblocks — compute, talent, or something else?这真正解除的瓶颈是什么——算力、人才，还是别的？
Trust and coordination, not compute or raw talent. The 22M problems weren't computationally infeasible one-by-one; the blocker was verifying contributions from strangers at scale, which Lean-based verification solved directly.
解除的是信任与协调瓶颈，而非算力或人才。2200 万道题逐一来看并非算力上不可行；真正的障碍是如何大规模验证陌生人的贡献，而这正是 Lean 验证直接解决的问题。
In-depth Analysis · Pros & Cons深入解读 · 优缺点
Fields medalist Terence Tao's 17-minute talk at SAIR's 2026 kickoff argues that mathematics — the most conservative academic discipline — is finally being reshaped, not by AI directly, but by formal verification as the enabling infrastructure. He backs this with a concrete case study: 50 collaborators solving 22 million algebra problems in three months, something no prior crowdsourced math project came close to.
Fields 奖得主陶哲轩在 SAIR 2026 启动活动上的 17 分钟演讲提出：数学——这个最保守的学术领域——终于开始被撬动，撬动它的不是 AI 本身，而是作为使能基础设施的形式验证。他用一个具体案例支撑这一论点：50 人协作三个月解决 2200 万道代数题，这是此前任何众包数学项目都望尘莫及的规模。
- Concrete, falsifiable case study具体、可证伪的实证案例Rather than speculating abstractly about AI and math, Tao anchors the entire argument in one dated, documented project with hard numbers (22M problems, 50 people, 3 months, day-16 metric), making the claim checkable rather than rhetorical.陶哲轩没有泛泛谈论 AI 与数学的关系，而是把整个论证锚定在一个有明确日期、有据可查的项目上，配有硬数字（2200 万题、50 人、三个月、第 16 天指标），使论断可核实而非空泛修辞。
- Correctly separates AI hype from the actual mechanism准确区分了 AI 炒作与真正起作用的机制He explicitly credits "mundane" tools — GitHub, Zulip, Lean — over AI as the real enabler, a counter-narrative move that resists the reflex to attribute progress to LLMs by default.他明确将 GitHub、Zulip、Lean 这类“平凡”工具而非 AI 列为真正的推动力，这种反直觉的表述有意抵制了将进展默认归功于 LLM 的思维惯性。
- Names a structural mechanism, not just an anecdote点明了结构性机制，而非仅是轶事The trust-barrier framing (verify-the-checker instead of verify-the-contributor) is a generalizable principle, not project-specific color — it explains why anonymous contributions suddenly became viable.“信任检查器而非信任贡献者”的框架是一个可推广的原理，而非仅限于该项目的细节描述——它解释了为什么匿名贡献突然变得可行。
- Honest about AI's current limits对 AI 现有局限保持坦诚Tao doesn't oversell LLMs — he states plainly that every mathematician who's tried them found the unreliability disqualifying, and frames AI's value as conditional on verification, not as an independent breakthrough.陶哲轩没有过度美化 LLM——他直言每个尝试过的数学家都认为其不可靠性是致命问题，并将 AI 的价值定性为依赖验证机制才能实现，而非独立性的突破。
- Single-domain generalization risk单一领域的推广风险The 22M-problem success comes from magma equational theory, a domain unusually amenable to combinatorial decomposition and Lean formalization. Whether this scales to less mechanizable fields like algebraic topology or analysis is untested and unaddressed.2200 万题的成功来自 magma 等式理论——一个异常适合组合式拆解和 Lean 形式化的领域。这种模式是否能推广到代数拓扑、分析学等难以机械化的领域，演讲中未经检验也未作说明。
- No cost/effort accounting缺少成本与投入的核算The talk celebrates the 3-month outcome but gives no sense of total person-hours, compute cost, or how much of the 50 collaborators' effort went into tooling versus actual problem-solving — making the productivity claim hard to benchmark.演讲庆祝了三个月的成果，却完全没有交代总人时投入、算力成本，或者 50 名协作者中有多少精力花在了工具搭建而非实际解题上——这使得生产力方面的论断难以量化对比。
- AlphaEvolve results are teased, not substantiatedAlphaEvolve 的结果只是预告，未经证实The infinite-dimensional optimization progress is explicitly withheld ("can't say more yet"), so the talk's most forward-looking AI claim currently rests on an unpublished, unverifiable promise rather than evidence.无穷维优化的新进展被明确按下不表（“暂时还不能说更多”），因此演讲中最具前瞻性的 AI 论断目前只是一个未发表、无法验证的预告，而非证据。
- Selection bias in the collaborator pool协作者群体存在选择偏差50 volunteers drawn largely from the Lean/formal-methods community are unusually motivated and technically literate; this doesn't demonstrate that formal verification alone would attract or sustain broader, less specialized participation.这 50 名志愿者大多来自 Lean/形式化方法社区，动机和技术素养都异于常人；这并不能证明形式验证本身就足以吸引或维持更广泛、专业程度较低的参与者。
Read this if you want a grounded, mechanism-first account of how math collaboration is actually changing — the Equational Theories Project is a genuinely novel data point, not hype. Caveat: it's one project in one unusually decomposable subfield, the AlphaEvolve infinite-dimensional claims are unpublished, and nothing here proves the model generalizes beyond algebra-flavored, combinatorially structured problems.
如果你想了解数学协作方式真正在如何转变，且看重机制而非炒作，这篇值得一读——等式理论项目确实是一个新颖的数据点，而非空谈。但需留意：它只是一个高度可拆解子领域中的单一项目，AlphaEvolve 在无穷维问题上的进展尚未发表，本演讲也没有证明这套模式能推广到代数、组合结构以外的数学问题。
Original Text原文
The English text on this side is an AI translation provided for convenience; the authoritative version is the source in the other language.
Terence Tao has 6 blackboards in his office, and he says he'll never give them up. But he just led 50 people using AI and code to solve 22 million math problems.
At the SAIR Foundation's "AI for Science: Kickoff 2026" event in February 2026, the Fields Medalist spent 17 minutes on one point: mathematics, a field whose way of working hasn't changed in centuries, is being levered open by new technology. And the key to that leverage isn't AI itself, but something most people have never heard of.
Original video link: https://www.youtube.com/watch?v=mS9Lr43cIB4
Key points at a glance:
Mathematics may be the most conservative discipline: textbooks from 200 years ago are still usable today, and mathematicians are the last academic group still using chalk and blackboards
There are structural reasons mathematicians don't like to collaborate: the barrier to entry is high, there is zero tolerance for error, and the workflow can't scale to internet scale
Formal verification is the "secret weapon" for large-scale mathematical collaboration — it breaks down the barrier of trust and makes anonymous contributions possible
The Equational Theories Project, led by Terence Tao, solved 22 million algebra problems within three months; previous projects of this kind had only handled about 20
LLMs can solve olympiad problems but still make mistakes on simple arithmetic — they must be paired with verifiers to be useful in mathematics
AI's greatest value for mathematics isn't replacing mathematicians on the hardest problems, but handling the vast number of medium-difficulty problems humans don't have the bandwidth to cover
Note: SAIR (Foundation for Science and AI Research) is a nonprofit foundation co-founded by Terence Tao dedicated to using AI to accelerate scientific discovery. This event was jointly hosted by SAIR and UCLA's IPAM.
A 200-year-old textbook still works today
At the start of his talk, Terence Tao showed a mathematics textbook written by Cauchy in 1826.
"Other than it's in French rather than English and it's not typeset using a modern computer language... it's completely usable today."
This 200-year continuity is one of mathematics's strengths. The Pythagorean theorem is a result from over two thousand years ago, and Tao said he himself often uses it in his own research. But the cost is that mathematicians are extremely conservative, almost the academic group least willing to embrace change.
He gave an interesting detail: mathematicians are probably the only academic discipline still clinging to blackboards and chalk. Other fields switched to PowerPoint and whiteboards long ago. Photographer Jessica Wynne even made a photo book specifically of mathematicians' blackboards, titled "Do Not Erase," which became an art book after publication.
Note: "Do Not Erase" was published by Princeton University Press in 2021 and features blackboard photos from over 100 mathematicians; Tao's own blackboard was photographed for it too.
And Tao himself?
"I have six blackboards in my own office. I love them. I will not give them up."
Why math can't do large-scale collaboration like other sciences
Tao showed a chart of the average number of authors per paper across disciplines over time. Collaboration numbers in other scientific fields have exploded. And math? It crept slowly from 1.5 people to 2.5 people.
He joked that it's not because mathematicians are antisocial, or rather, "not just because of that." The real reasons are three:
First, the barrier is too high. You typically need a PhD in mathematics to even understand the problem you're working on.
Second, the correctness requirement is extreme. If you crowdsource a proof, and 1 out of 100 contributions is wrong, the whole proof is ruined.
"If you try to crowdsource a proof and there's 100 contributions and one of them is incorrect, you destroy the whole proof."
Third, the workflow doesn't scale. Mathematicians' core mode of working is two or three people standing in front of a blackboard discussing — that can't scale to 100 people collaborating online.
But other sciences are already doing this, and thriving.
Is mathematics missing out on something?
From one problem at a time to a million problems at a time
Tao said change is happening. He used a sharp framework to describe it: past mathematical research was the "case study" model — pick one problem at a time, spend months producing a paper, then move to the next. Now a "large-scale survey" model is emerging, handling hundreds or even thousands of problems simultaneously. Maybe not all of them can be solved, but you can report interesting statistical patterns across the group of problems.
The pool of participants is also widening. "Citizen science" is already well established in other disciplines; mathematics is only just beginning to see "citizen mathematics."
Note: Citizen science refers to non-professional scientists participating in research projects — for example, astronomy enthusiasts helping classify galaxy images. This model has rarely existed in mathematics before now.
As for AI? Tao's phrasing here is interesting:
"We've discovered lots of incorrect ways to use machine learning and AI, but we're just beginning to get some useful mileage out of these tools."
And what makes all of this possible is a "secret weapon."
The secret weapon: formal verification
This secret weapon isn't AI — it's formal verification.
Put simply, formal verification is a special kind of computer language that can take a piece of mathematical reasoning and automatically determine whether it's correct. Tao said this one capability "filters out a huge amount of junk," removing the biggest obstacle that previously blocked new workflows.
Why does this matter so much? Because it directly solves the earlier problem of "one wrong contribution out of 100 ruins the whole proof." With automatic checking, you no longer need to trust every contributor — you only need to trust the verification system.
Note: The most active tool in the field of mathematical formalization right now is Lean, a proof assistant language developed by Microsoft Research. It doesn't just verify whether a proof is correct — it also works like an IDE, flagging in real time where a step has gone wrong as you write the proof.
22 million algebra problems, 50 people, three months
Tao spent the most time on this case study: the Equational Theories Project.
He launched this project at UCLA, with 50 collaborators participating in total. But most of these people he had never met in person — he got to know them through the project; most weren't professional mathematicians either, but computer scientists, graduate students, undergraduates, and he said there were possibly even high schoolers.
The project's task: it programmatically generated 22 million algebraic implication problems. For example, if an operation satisfies commutativity (a*b = b*a), can you deduce it also satisfies associativity ((a*b)*c = a*(b*c))? The answer is no. But there are 22 million problems like this.
Note: To be precise, this covers the pairwise implications between the equational laws of 4,694 magmas (algebraic structures with a single binary operation), totaling 22,028,942 pairs. The project launched on GitHub on September 25, 2024, and the final paper was uploaded to arXiv in December 2025.
Taken individually, each problem might take a graduate student in algebra an hour to solve. But 22 million of them?
"I don't have 22 million grad students."
You could say "just crowdsource it," but who grades 22 million problems? Previous studies of this kind had handled at most 20 problems.
They finished in three months. Every single one had either a proof or a disproof.
How did they do it? All proofs were stored on GitHub and had to be formalized in the Lean language, so correctness could be automatically verified. Collaborative discussion happened on Zulip (an open-source Slack-like platform). Some people wrote human-readable proofs, others translated them into Lean code; some wrote programs to tackle problems in bulk, handling 100,000 at a time; others converted computer proofs back into human-readable proofs. There was a lot of back-and-forth iteration — improvised on the fly, but it worked extremely well.
Why this project succeeded
Tao summarized several key factors.
First, modularity. The 22 million problems naturally broke down into subtasks, and each person could claim a batch to work on. Some people specialized in writing human proofs, others in Lean translation — you didn't need to understand the whole project to contribute. He compared it to "a modern software development project."
Second, there was a clear metric. On day 16 of the project, only 888 of the 22 million implications remained unsolved. That number became everyone's target, to push it down. Some ideas could knock out a large batch at once, others were less successful. But no global coordination was needed — everyone was spontaneously pushing the number down. Tao said the participants' spontaneous action "was really quite fun to watch."
Third, and most crucial: formal verification broke down the barrier of trust.
The old model of mathematical collaboration was: either check someone else's work line by line, or trust them based on reputation. But this project received a huge number of contributions from strangers, some of whom had never appeared in the math community before. That was fine — every submission had to pass Lean's automatic verification. Anonymous contributions? Fine. Untrusted contributions? Also fine.
And formal verification made discussions extremely precise. For instance, if someone submitted a nine-step proof where the first eight steps passed and Lean flagged an error on the ninth, you could discuss that one tiny step with the author directly. Previously, without a shared precise language, it was hard to pin down exactly where things got stuck; now you can have technical conversations at the "atomic level."
Throughout the project, AI tools like automated theorem provers were used too, but Tao candidly said:
"Actually it was the more mundane technologies, things just like GitHub and this discussion group at Zulip. Basic collaboration platforms were just incredibly useful and essential."
Note: Zulip is an open-source group discussion platform, similar to Slack but with a distinctive "topic threading" feature that's particularly suited to technical discussions. Zulip is the main communication platform for the Lean mathematics community.
LLMs can solve olympiad problems, but still get multiplication wrong
In the second half of the talk, Tao turned to AI and large language models.
LLMs are getting more and more powerful — they can solve math olympiad problems, and sometimes answer very deep math questions. But they make mistakes, and often very basic ones. Tao showed an example: an LLM was asked what 7×4+8×8 equals, and got it wrong. After being pointed out, it apologized, then gave the correct answer.
Every mathematician has tried using an LLM. And the conclusion?
"Every mathematician has tried using these and has eventually found that the unreliability is too great of an issue."
But what if you combine an unreliable LLM's output with a verifier? Let the LLM generate mathematical output, have the verifier check whether it's correct; keep it if correct, and if not, feed the error message back to the LLM so it can correct itself. This "generate → check → feedback → correct" loop sometimes works.
Tao is collaborating with Google DeepMind on their latest tool, AlphaEvolve. This tool isn't just an LLM — underneath it also runs a genetic algorithm.
Note: AlphaEvolve is an "evolutionary coding agent" developed by Google DeepMind, combining an LLM's (Gemini) code-generation ability with evolutionary algorithms, solving math and science problems by continuously proposing, testing, and optimizing code solutions. It was publicly announced in May 2025, and in November of that year, Tao and colleagues published a paper on arXiv using AlphaEvolve to tackle 67 math problems.
He gave an example: if you have 11 regular hexagons, what's the smallest regular hexagon you can pack them into? There were previous best records found by humans, and AlphaEvolve broke these records by having the LLM keep trying, getting feedback, and evolving the code.
But these are just test cases. Packing problems are essentially finite-dimensional optimization, just a small subclass of the problems mathematicians care about. Tao revealed they've also made new progress on infinite-dimensional optimization problems, but "unfortunately, I can't say more for now. Stay tuned — we'll have a paper out in a few weeks."
Not here to take a slice of the cake, but to make the cake bigger
Wrapping up the talk, Tao summarized AI's impact on mathematics.
Scenarios where it's already proving useful:
Writing code is far easier than it used to be
Literature review is already a very useful application.
There are scattered cases showing AI can discover new mathematical conjectures from datasets.
AI is a great "universal translator," helping mathematicians communicate with the public and other disciplines, since each has its own system of terminology.
But to reach more advanced applications, rigorous verification is essential. AI helping individual mathematicians on their own has some value, but it's most effective when combined with a broader collaborative system, where it can fill in the missing links in that collaboration.
We can only use the AI as far as you can trust its outputs, or at least check them. Any further and it's just too risky.
He then raised a view that differs from the common assumption. The most obvious use people imagine for AI is having it replace mathematicians at what they do best, cracking hard problems with creative new techniques. But there's an "orthogonal" use that will likely be more productive, at least in the medium term.
Mathematics has a huge "long tail of medium-difficulty problems," like those 22 million algebra questions. There aren't enough people to work through them one by one, but AI can be set loose first to knock out the easy ones, then escalate the truly hard ones to human experts.
AI should be used to not compete with the pie of work that humans already do, but to enlarge the pie and create more tasks — make more objectives economically feasible.
He added in closing: these applications are all highly context-dependent, not plug-and-play. You need to know when and how to use them.
Full talk video: https://www.youtube.com/watch?v=mS9Lr43cIB4
陶哲轩办公室有 6 块黑板，他说绝不放弃。但他刚带 50 个人用 AI 和代码解决了 2200 万道数学题。
这位 Fields 奖得主在 2026 年 2 月的 SAIR 基金会“AI for Science: Kickoff 2026”活动上，用 17 分钟讲了一件事：数学这个几百年没变过工作方式的领域，正在被新技术撬动。 而撬动它的关键，不是 AI 本身，而是一个大多数人没听说过的东西。
原始视频链接：https://www.youtube.com/watch?v=mS9Lr43cIB4
要点速览：
- 数学可能是最保守的学科：200 年前的教材今天还能用，数学家是最后还在用粉笔黑板的学术群体
- 数学家不爱协作有结构性原因：准入门槛高、容错率为零、工作流无法扩展到互联网规模
- 形式验证是大规模数学协作的“秘密武器”，它打破了信任壁垒，让匿名贡献成为可能
- 陶哲轩主导的等式理论项目在三个月内解决了 2200 万个代数问题，此前同类项目只处理过约 20 个
- LLM 能解奥赛题但连简单算术都会出错，必须配合验证器才能在数学中发挥作用
- AI 对数学最大的价值不是替代数学家攻克最难的问题，而是处理人类没精力覆盖的海量中等难度问题
注： SAIR（Foundation for Science and AI Research）是陶哲轩联合创办的非营利基金会，致力于用 AI 加速科学发现。本次活动由 SAIR 与 UCLA 的 IPAM 联合举办。
200 年前的课本，今天还能用
陶哲轩在演讲开头展示了一本 1826 年 Cauchy 写的数学教科书。
除了是用法语写的、不是用现代排版工具排的，跟我们今天给研究生用的几乎一模一样。 （“Other than it's in French rather than English and it's not typeset using a modern computer language... it's completely usable today.”）
这种 200 年的连续性是数学的力量。勾股定理是两千多年前的成果，陶哲轩说他自己的研究中经常使用。但代价是：数学家极度保守，几乎是最不愿拥抱变化的学术群体。
他举了一个有趣的细节：数学家恐怕是唯一还守着黑板和粉笔的学术学科了。其他领域早就换成了 PPT 和白板。摄影师 Jessica Wynne 甚至专门拍了一本数学家黑板的摄影集《Do Not Erase》（别擦掉），出版后成了一本艺术画册。
注：《Do Not Erase》由 Princeton University Press 于 2021 年出版，收录了 100 多位数学家的黑板照片，陶哲轩的黑板也被拍进去了。
而陶哲轩自己呢？
我办公室有 6 块黑板。我爱它们。我不会放弃的。 （“I have six blackboards in my own office. I love them. I will not give them up.”）
为什么数学不能像其他科学那样搞大规模协作
陶哲轩展示了一张各学科论文平均作者数的变化图。其他科学领域的协作人数在爆炸式增长，数学呢？从 1.5 人缓慢爬到了 2.5 人。
他自嘲说，不是因为数学家反社会，或者说“不只是因为反社会”。真正的原因有三个：
第一，门槛太高。 你通常得有数学博士学位才能理解自己在做什么问题。
第二，正确性要求极端。 如果你众包一个证明，100 份贡献里有 1 份是错的，整个证明就废了。
如果你尝试众包一个证明，100 个贡献中有一个是错误的，就毁掉了整个证明。 （“If you try to crowdsource a proof and there's 100 contributions and one of them is incorrect, you destroy the whole proof.”）
第三，工作流没法扩展。 数学家的核心工作方式是两三个人站在黑板前讨论，这没法 scale 到 100 人在线协作。
但其他科学已经在这样做了，而且蓬勃发展。
数学是不是错过了什么？
从一次一题到一次百万题
陶哲轩说，变化正在发生。他用了一个精辟的框架来描述：过去的数学研究是“案例研究”模式，一次挑一个问题，花几个月产出一篇论文，再去做下一个。现在开始出现“大规模调查”模式，同时处理数百甚至数千个问题。也许不能全部解决，但可以报告这些问题群体的有趣统计规律。
参与者也在拓宽。其他学科的“公民科学”已经很成熟了，数学才刚开始出现“公民数学”。
注： 公民科学（citizen science）指非专业科学家参与科研项目，比如天文爱好者帮助分类星系图像。数学领域此前很少有这种模式。
至于 AI？陶哲轩的措辞很有意思：
我们发现了很多使用机器学习和 AI 的错误方式，但才刚开始从这些工具中获得一些有用的价值。 （“We've discovered lots of incorrect ways to use machine learning and AI, but we're just beginning to get some useful mileage out of these tools.”）
而让这一切成为可能的，有一个”秘密武器”。
秘密武器：形式验证
这个秘密武器不是 AI，而是形式验证（formal verification）。
简单说，形式验证是一种特殊的计算机语言，能接收一段数学论证，自动判断它对不对。陶哲轩说，这一个能力就“过滤掉了大量垃圾”，移除了此前阻碍新工作流的最大障碍。
为什么这么重要？因为它直接解决了前面提到的“100 份贡献里 1 份错误就毁掉整个证明”的问题。有了自动检查，你不再需要信任每个贡献者，只需要信任验证系统。
注： 目前数学形式化领域最活跃的工具是 Lean，由微软研究院开发的证明助手语言。它不仅能验证证明对不对，还能像 IDE 一样在写证明过程中实时提示哪一步出了问题。
2200 万道代数题，50 个人，三个月
陶哲轩花了最多篇幅讲这个案例：Equational Theories Project（等式理论项目）。
他在 UCLA 发起了这个项目，共 50 位协作者参与。但这些人大多数他从未见过面，是通过项目才认识的；大多数也不是专业数学家，而是计算机科学家、研究生、本科生，他说甚至可能有高中生。
项目的任务是：程序化生成了 2200 万道代数蕴含关系问题。比如，如果一个运算满足交换律（a*b = b*a），能推出它也满足结合律（(a*b)*c = a*(b*c)）吗？答案是不能。但这样的问题有 2200 万个。
注： 准确地说，是 4694 个 magma（只有一个二元运算的代数结构）等式定律之间的两两蕴含关系，共 22,028,942 对。项目于 2024 年 9 月 25 日在 GitHub 上启动，最终论文于 2025 年 12 月上传 arXiv。
单独来看，每道题可能一个代数方向的研究生花一小时就能解。但 2200 万道？
我可没有 2200 万个研究生。 （“I don't have 22 million grad students.”）
你可以说“那就众包吧”，但谁来批改 2200 万道题？以前同类型的研究最多处理过 20 个问题。
他们三个月就做完了。每一道都有证明或反证。
怎么做到的？所有证明存在 GitHub 上，必须用 Lean 语言形式化，这样就能自动验证正确性。协作讨论在 Zulip（一个开源的类 Slack 平台）上进行。有人写出人类可读的证明，有人把它翻译成 Lean 代码；有人写程序批量攻克问题，一次处理 10 万道；有人则把计算机证明转化回人类证明。大量来回迭代，虽然是即兴摸索出来的，但效果极好。
为什么这个项目能成功
陶哲轩总结了几个关键因素。
第一是模块化。 2200 万个问题天然地拆分成子任务，每个人可以认领一批来做。有人专写人类证明，有人专做 Lean 翻译，不需要理解项目全貌就能贡献。他类比说，”就像现代软件开发项目”。
第二是有一个明确的指标。 在项目第 16 天，2200 万个蕴含关系中只剩 888 个未解决。这个数字就是所有人的目标，把它往下推。有些想法一次能消掉一大批，有些没那么成功。但不需要全局协调，每个人都在自发地把数字往下推。陶哲轩说，参与者的自发行动“看着真的很有趣”。
第三，也是最关键的：形式验证打破了信任壁垒。
以前数学协作的模式是：要么逐行检查别人的工作，要么靠声誉信任对方。但这个项目收到了大量来自陌生人的贡献，有些人从未在数学界露过面。这没关系，所有提交都必须通过 Lean 的自动验证。匿名贡献？可以。不受信任的贡献？也可以。
而且形式验证让讨论变得极其精确。比如有人提交了一个九步证明，前八步都通过了，第九步 Lean 报错。这时候你可以就那一个微小的步骤跟作者讨论。以前没有共同的精确语言，很难定位到底卡在哪一步；现在可以在“原子级别”上进行技术对话。
整个项目中，虽然也用了自动化定理证明器之类的 AI 工具，但陶哲轩坦言：
实际上起作用的是更平凡的技术，就是 GitHub 和 Zulip 这些基本的协作平台，它们简直太有用了。 （“Actually it was the more mundane technologies, things just like GitHub and this discussion group at Zulip. Basic collaboration platforms were just incredibly useful and essential.”）
注： Zulip 是一个开源的群组讨论平台，类似 Slack 但有独特的”话题线程”功能，特别适合技术讨论。Lean 数学社区的主要交流平台就是 Zulip。
LLM 能解奥赛题，但连乘法都会算错
演讲进入下半段，陶哲轩转向 AI 和大语言模型。
LLM 越来越强大了，能解数学奥赛题，有时能回答很深的数学问题。但它们会犯错误，而且经常是非常基础的错误。陶哲轩展示了一个例子：某 LLM 被问 7×4+8×8 等于多少，算错了。被指出后道歉，然后给出了正确答案。
每个数学家都试过用 LLM。结论呢？
每个数学家最终都发现，不可靠性是一个太大的问题。 （“Every mathematician has tried using these and has eventually found that the unreliability is too great of an issue.”）
但如果把不可靠的 LLM 输出和一个验证器结合起来呢？让 LLM 生成数学输出，验证器检查是否正确；正确就保留，不正确就把错误信息反馈给 LLM 让它纠正。这个“生成→检验→反馈→纠正”的循环，有时候能跑通。
陶哲轩正在跟 Google DeepMind 合作他们最新的工具 AlphaEvolve。这个工具不只是 LLM，底层还有遗传算法。
注： AlphaEvolve 是 Google DeepMind 开发的”进化式编程智能体”，结合 LLM（Gemini）的代码生成能力和进化算法，通过不断提出、测试、优化代码方案来解决数学和科学问题。2025 年 5 月公开宣布，同年 11 月陶哲轩等人在 arXiv 发表了使用 AlphaEvolve 攻克 67 个数学问题的论文。
他举了一个例子：如果你有 11 个正六边形，能装进去的最小正六边形多大？以前有人类找到的最优记录，AlphaEvolve 通过让 LLM 不断尝试、获取反馈、进化代码，打破了这些记录。
但这些只是测试案例。堆叠问题本质上是有限维优化，只是数学家关心的问题的一个很小的子类。陶哲轩透露，他们在无穷维优化问题上也有了新进展，但”很遗憾，暂时还不能说更多。请关注，几周后我们会发论文。”
不是来抢蛋糕的，是来把蛋糕做大的
演讲收尾，陶哲轩总结了 AI 对数学的影响。
已经在发挥作用的场景：
- 写代码比以前容易太多了
- 文献综述已经是很好用的应用
- 有零星案例显示 AI 能从数据集中发现新的数学猜想
- AI 是很好的“万能翻译器”，帮助数学家跟公众和其他学科沟通，因为各自的术语体系不同
但要获得更高级的应用，必须依赖严格的验证。AI 单独辅助个体数学家有一定帮助，但和更广泛的协作体系结合时效果最大，它能填补协作中缺失的环节。
我们只能在信任 AI 输出的范围内使用它，或者至少能检查它。超出这个范围就太冒险了。 （“We can only use the AI as far as you can trust its outputs, or at least check them. Any further and it's just too risky.”）
然后他提出了一个和常见想象不同的观点。大家最容易想到的 AI 用途，是用 AI 替代数学家做他们最擅长的事，用创造性的新技术攻克难题。但有一个“正交”的用途，至少在中期内会更有生产力。
数学中存在一条巨大的“中等难度问题长尾”，就像那 2200 万道代数题。人类没有人力一个个去做，但可以让 AI 先跑一遍，把简单的都解决掉，然后把真正难的上报给人类专家。
AI 不应该跟人类已经在做的工作竞争，而应该把蛋糕做大，创造出更多任务，让更多目标在经济上变得可行。 （“AI should be used to not compete with the pie of work that humans already do, but to enlarge the pie and create more tasks — make more objectives economically feasible.”）
他最后补充：这些应用都非常依赖具体场景，不是即插即用的。得知道什么时候该用、怎么用。
完整演讲视频：https://www.youtube.com/watch?v=mS9Lr43cIB4
See all posts