又是一篇谈 AI 和数学的文章，我知道。先别划走，开头是一份流水账：10 月 1 日到 6 日，六天，数学圈里出了七件事。

每件事单拎出来都不算大。放在一起看，问的是同一个问题：证明变便宜了，数学家的活到底是什么？

我想借一本老书来回答。Saunders Mac Lane 的《数学：形式与功能》，1986 年出版，476 页。他 2005 年就去世了，没写过一个字关于 AI，我也没找到有人把这本书拿进今年的讨论。所以下面一半是书里的内容，一半是我的读法，我会标出来。

答案我先说：机器正在把“形式”做完，“功能”还得有人认领。

先把事实摆平，免得有人说我嘴硬。

一年前，是个笑话。2025 年 10 月，OpenAI 的一位副总裁发推说，GPT-5 找到了 10 道 Erdős 未解问题的答案。维护 Erdős 问题网站的 Thomas Bloom 回了一句：这是严重的误述。网站上标“开放”，只表示他本人不知道有人解过。GPT-5 找到的，是他漏掉的旧文献。推文删了，DeepMind 的 Hassabis 说这很尴尬。（据 Futurism 等多家报道）

七个月后，笑话变成了新闻。2026 年 5 月 20 日，OpenAI 的一个模型推翻了 Erdős 的单位距离猜想：平面上放 n 个点，距离恰好为 1 的点对，最多能有多少对？Erdős 猜它几乎就是 n 的量级。模型造出来的例子，指数严格大于 1。数学家 Will Sawin 随后把数字算了出来：多于 n^1.014 对。

背后是代数数论：造出次数很大、判别式很小的代数数域，靠 Golod-Shafarevich 判据保证它存在。一个组合几何的老问题，被数论的工具打穿了。

同一天，九位数学家写了份说明：简短，消化过，人工核验过。作者里有 Gowers，也有 Bloom，就是去年纠正 OpenAI 的那位。

再往后几周，一件接一件。1939 年提出的 Jacobian 猜想，在三个复变量的情形被找到了反例，是 Alpöge 借助 AI 找到的，不用信任何人，直接算就能验证。Sendov 猜想有了 AI 给出的证明，Tao 把它化简到只用基本的复分析和 Maclaurin 不等式。9 月 4 日，Anthropic 的模型用 11 天，把费马大定理的证明整个翻译成了 Lean。Kevin Buzzard 自己也在做同一件事，他那篇博文的标题是：Anthropic 抢在我前面了。

十月的头一个星期，事情更密了。

10 月 4 日，KLS 猜想有了完整证明。这是高维几何里 1995 年留下的核心问题：任何各向同性的对数凹分布，Cheeger 常数都有一个和维数无关的正下界。Zhao Song 和 Xinzhi Zhang 把 10 月 1 日挂出的 O(4^{log* n}) 版本改成了 O(1)。同一天，Bizeul、Klartag 和 Lehec 以他们的判据为关键一步，挂出了另一份证明。

两篇论文都在致谢里交代了 AI 的用法。Song 和 Zhang 列出了所用的四个模型，说从 7 月 28 日起，他们和 AI 工具一起探索了一百多条路，由人决定先试哪些。Bizeul、Klartag 和 Lehec 写得更直白：大部分证明和数学想法由 ChatGPT 找到，只有 suspension 这个想法来自作者；作者的角色，主要是读懂这些证明，改进写法。

10 月 5 日，Josh Alman 和 Virginia Vassilevska Williams 挂出一篇论文：3SUM 有了确定性的 O(n^1.9992) 算法，APSP 有了 O(n^2.9995) 算法。论文称，这推翻了 3SUM 假设和 APSP 假设，它们是细粒度复杂性里压了几十年的两块基石。

论文前言还写了一件事：这个算法是 Claude 发现的。Anthropic 的一位员工用内部研究模型研究密码学里的开放问题，让它验证并改进一个构造，模型却另外走出了这个算法，先是平均情形，再是最坏情形。整个会话用了 1600 万个输出 token，没有人为输入。9 月，Anthropic 在保密协议下把它交给了两位作者。作者再去读懂它、简化它、加强它，主要结果还由 Claude 用 Lean 4 验证。作者声明对论文负全责。这两篇都刚挂出，还没有同行评审。

它也有失手的时候。First Proof 是 11 位数学家出的十道没发表过的研究级问题。第一批（2 月）出题人自己判下来，明确做对的大约 2 道，厂商自报了 5 到 6 道，争的是中间有多少人的手。（据 Scientific American 报道）9 月 8 日那件，是 OpenAI 宣布给带光滑外力的 Navier-Stokes 方程造出了有限时间爆破，我之前写过。到今天，没有独立核验的结论。

说句公道话，一年前，这类消息大半可以当营销看。现在不行了。单位距离那份核验，是 Gowers、Bloom 这些最不好糊弄的人，亲自下场写的。

所以我不打算在“AI 行不行”上花笔墨。Tao 今年 ICM 的报告，一上来也说他不谈这个：他直接假设这些能力会到来，转去问另一个问题，数学研究的目标和价值，究竟是什么。

把这个月的文章和帖子读一遍，会发现大家吵的不是 AI 行不行，吵的是数学的产出到底是什么。

Buzzard 10 月 1 日那篇，立场最直白。他说他入行是冲着定理总数去的。数学是无穷的，指数增长也追不上，AI 多找出一些定理，是好事。他不买 Thurston 那一套。Thurston 在 1994 年写过一篇名文，大意是：数学家不是在完成定理和证明的产量指标，成败看人们是否因此想得更清楚。Tao 的 ICM 报告又引了它。Buzzard 还主张厂商把手里的证明公开，人类会慢慢读懂。

9 月 11 日，最初 25 位菲尔兹奖得主联名发了一封信，题目叫 A Severe Misalignment of AI in Mathematics。核心一句：解决问题，只是通向概念理解这个首要目标的工具，也只是它的替代指标。厂商赶着发布，不写，不署名，不讲，人类传承的链条就断了。信没有要求禁止谁，要求的是对话。

Gowers 没有签这封信。他说数学家站在一条光谱上，一头重解题，一头重理解，信把理解排在解题上面，不公平。他真正担心的是另一件事：本来会去读博、将来接过这门手艺的人，会不会不来了。

Litt 的看法是，数学从来不只是说出真句子，还包括提出对的问题、困惑、跌跌撞撞。他 9 月 13 日给了一套办法：博士论文换成口试答辩，招聘看报告和讨论，不数论文。

网上吵得更热闹，评论区像一锅煮开的粥。那封信发到 Hacker News 上，1,242 分，1,215 条评论。有人说它针对的不是 AI，是只要头条的公司做法；有人嫌“错位”一词太重；也有人拿望月新一的 abc 证明做类比：看不懂的证明，同样催生了一大批研究。B 站有条视频，《AI开始暴力破解数学难题之后，数学家为什么集体反对？》，9 月 18 日发的，约 29 万播放，2,011 条评论。

把这些声音排成一条线：

两头的人，其实都不否认 AI 能做事。真正的分歧是：数学这件事，它的功能是什么？是产出一批可核验的真命题，还是让人更清楚地理解世界？

这正是 Mac Lane 四十年前问的问题。

Saunders Mac Lane（1909-2005），1945 年和 Samuel Eilenberg 一起写下范畴论的奠基论文，做过美国数学会会长，1989 年拿了美国国家科学奖章。他的博士论文是 1933 年在哥廷根答辩的，题目翻译过来是《逻辑演算中的缩短证明》。导师是 Paul Bernays，Weyl 是考官。

一个博士论文研究缩短证明的人，晚年写了本书，问数学到底是什么。1986 年，他出了《数学：形式与功能》（Springer）。这不是一本哲学专著，十二章里多数在讲数学本身：整数和有理数，几何，实数，函数与群，微积分，线性代数，空间，力学，复分析与拓扑，集合、逻辑与范畴。最后一章，叫“数学网络”。

引言里，他先说这本书的意图，然后问：

他接着说，要回答它，得先看清数学本身：一种数学哲学，如果不是建立在对数学本身的考察上，就没有说服力。他还点了名，说维特根斯坦等哲学家在这一点上失败了。

他的答案有个草图版，写在 1981 年的一篇文章里（《数学模型：数学哲学的一个草图》，Amer. Math. Monthly 88）。1986 年的书思路一脉相承，在第一章 §I.11 给了更长的一张表。

数学从人的活动里来。1981 年那篇列了十项：

清单里有一项值得多看一眼：证明。在他这里，证明是十种人类活动之一，通向逻辑。它是数学的一部分，不是数学的全部。

活动留下来的，是些模糊的念头，比如“下一个”“对称”“逼近”（第一章那张表里的例子）。数学做的事，是把这些念头里普遍的、不任意的部分剥出来，再形式化，写成公理、定义、定理。然后，形式再回到活动里，帮人看清那些活动。他的一句总结是：数学是形式的，但不只是“形式主义”的，因为这些形式来自人的活动，又用来理解这些活动。

他对几个主流学派都不客气。逻辑主义、形式主义、直觉主义、柏拉图主义、经验主义，他说没有一个给出了令人满意的分析。把数学等同于集合论里能推出的东西，他叫“一边倒”：集合论对大多数数学的实践基本无关，也解释不了数学在科学里为什么这么好用。

他把基础叫作组织数学的提议，不叫地基。数学不是一座建在一套公理上的金字塔，是一张网。

“形式来自活动，又回到活动”，这话能不能说得硬一点？拿十项里最老的一项，数数，做个实验。

数数留下的念头是“下一个”。把它形式化，就是 Peano 公理：有个起点 0；每个数有唯一的后继 S；0 不是任何数的后继；不同的数后继不同；再加一条归纳公理。问题是，这几条，把“数数”说死了吗？答案有两个，方向相反。

下面两条定理带证明。证明可以跳，结论和图别跳。

换句话说：只要你肯用“任意子集”这种说法，数数就被说死了。天下只有一个自然数列，和你用什么材料搭它无关。

可一阶逻辑只允许对每个公式写一条归纳公理（“公理模式”），谈不了“任意子集”。

两条定理合起来，是一笔小小的交易。想把“数数”的意思锁死，得用能谈“所有子集”的语言，而这种二阶逻辑（按完全语义）没有既可靠又完备的机械证明演算（这是哥德尔不完备定理的推论）。用机器能全部推完的一阶语言，又锁不死。精确到唯一，和机械可穷尽，没法两样都要。

今天的证明助手用的是更强的类型论，自然数是内置的，这笔交易没有因此消失。机器检查的是你写下的那条形式命题，它是不是你真正想问的那个问题，没有哪个系统能替你担保。我之前说 Lean 文件要有人逐字审，说的就是这个。

Mac Lane 在同一篇文章里分过这两类结构：自然数、有理数、实数、欧氏几何，本意是唯一的；群、环、拓扑空间，本来就是要有很多模型的。数数属于前一类，所以定理 1 对它才要紧。

他还写过一句，大意是：公理系统编码了活动里更深的、不显然的性质。这两条定理像是这句话的精确版：形式能抓住活动的多少，取决于你愿意付出什么代价；至于抓住了没有，只能回到活动本身去判断。（最后一句是我的读法）

Tao 的 ICM 报告里有一段历史。1901 年有罗素悖论，1931 年有哥德尔不完备定理，数学在 1900 到 1930 年间经历了基础危机。危机的产物，是一套明确的、标准化的基础框架：数学的对象和推理规则摆在明面上，可以检查，可以教，后来证明还可以被机械化。

他接着说，现在我们进入了一个同等动荡的时期。不同的是，这回被压力测试的不是真理的基础，而是价值和惯例的隐含框架：什么算贡献，奖励什么，什么算懂了，以及谁，或者什么，做了这件事。

换成 Mac Lane 的词：上一次危机，吵的是 form。这一次，吵的是 function。

Mac Lane 对 form 的标准，其实早就把今天写进去了。书的第 377 页，他说一个数学证明是严格的，当它（或者可以）被写成一阶谓词语言里的形式证明；实际中的证明是一份草图，详细到足以让人把它常规地翻译成形式证明。

“常规地翻译”，在 2026 年成了真正的常规。9 月，Anthropic 的模型花 11 天，把费马大定理的证明整个翻成了约 1340 万行 Lean。形式化阵营的旗手之一 Buzzard 评价说：他有 99.9% 的把握证明没问题；这个形式化只是忠实地跟着早期文献，没有增加任何新东西。像是花 11 天，把一本大家早就信的书，重新誊了一遍。他自己的 FLT 项目要做的，是另一件事：一份人能探索的动态文档。

严格买到了，理解一分没多。Mac Lane 在 1981 年那篇的第 9 节，早就讲过严格不够。他说，一种平衡的数学哲学，要在严格之外补上三样：广度、清晰、深度。清晰，是超越严格的精确，是对观念的清楚排序。深度，是抓住问题底下那些不显然的、更基本的结构，比如群论之于对称。

今年数学圈的几个新词，几乎都能在这三样里找到位置。Tao 说 AI 抛光过的证明读着容易、学着难，是清晰出了问题。他说的消化、定论化，是广度和深度。

Mac Lane 自己做过一次最漂亮的“消化”。1963 年，他在《自然的结合律与交换律》里处理张量范畴。在那里，结合律 (A⊗B)⊗C ≅ A⊗(B⊗C) 不是等号，只是一个同构。四个对象相乘，有 5 种括法；五个，14 种；六个，42 种；七个，132 种。每两种括法之间都能用结合同构连起来，可不同的连法，会不会给出同一个结果？这是无穷多个问题。

无穷个检查，压成一个。这就是消化。今年 7 月，Tao 把 Jacobian 反例拆成三条性质，逐条讲清；8 月，他把 Sendov 的证明化简到只用基本的复分析。他做的是同一种事，只是没有定理的名字。

Tao 把“解决问题”这个目标改了五稿。最终版是：解出未解的问题，验证它，讲清楚，让社群消化、接受，并入这个领域的定论。他把整个过程排成五个环节：生成、验证、表述、发表、消化。

AI 已经接管了前两格，正在往第三格走。第四、五格，是最慢的一段，Tao 说也是最有价值的一段。他还有个观察：AI 做数学这件事本身，靠的就是人类几百年来一遍遍重写出来的标准理论，训练数据，说白了就是定论化的产物。

他的另一个判断，更扎心：我们从“证明稀缺”走向“证明过剩”。期刊、优先权惯例、聘任晋升标准、奖项，乃至“研究计划”这个概念本身，都是在稀缺的假设下设计的。过剩了，它们就开始变形。

这些变形，没有一个是在争“AI 行不行”。每一个都在问同一件事：这个制度，原本是替什么功能服务的？

Mac Lane 不会意外。他的看法是，基础只是组织数学的提议，数学长了，提议就要换。固定的基础，会把新形式的发现挡在门外。（据 McLarty 对该书的述评）

回到题目。以下是我借 Mac Lane 的框架做的推演，不是他的结论，三点。

第一，Buzzard 的反驳站得住。数学是无穷的，定理总数是实打实的、可度量的东西，“理解”是个说不清的词。而且 Mac Lane 也不是纯粹以人为中心的。他 1981 年给数学下的定义是：发现支撑着世界、以及世界里人类活动的形式结构，一层一层往上。“世界”这个词，在里面。

第二，他的十项活动是身体的、古老的：数数，量，运动，造形。今天的代数几何离它们很远。他的办法是观念建在观念上，层层叠。但 AI 能不能在形式和形式之间自己往上叠，不需要新的人类活动，这本书没回答。Alman 他们那篇的前言是个现成的案例：模型是在做别人布置的任务时，自己拐出了这个算法，没有人为输入。题目是人给的，路是机器走的。

第三，哲学界对他的读法也不统一。McLarty 把他看作自然主义哲学家的典范；2025 年，Skowron 在 Philosophia Mathematica 上论证，他说的“观念”其实近似理想存在，和他反对柏拉图主义的表态相悖。

回到开头那六天。arXiv 在限流，Bloom 在关站，Córdoba 说现在没法评论，Buzzard 在悲伤和乐观之间表态。KLS 和 3SUM 那两篇论文的作者，在致谢里用差不多的话交代了自己的角色：读懂，简化，把写法改好。每个人都在给手里的某一个“形式”，重新找它的功能：论文，问题清单，博士论文，会议。

Tao 说，得把那些没写下来的目标写明白。这是个写作任务。Mac Lane 在 1986 年做过一次：他没有等哲学家，自己把数学从头走了一遍，再回头问，这一切是干什么用的。

AI 把“证明”这项活动，做得越来越好。可证明只是他清单里十项之一。

“形式可以交给机器，
功能还得有人认领。

如果有一天，机器自己长出了新的“活动”，自己往上叠观念，那就是另一本书的问题了。

Yes, I know: another essay about AI and mathematics. Don’t scroll past just yet. It opens with a plain record of events: in the six days from October 1 to 6, seven things happened in the mathematical world.

None of them is big on its own. Taken together, they ask the same question: now that proofs are cheap, what exactly is a mathematician’s job?

I want to answer it with an old book: Saunders Mac Lane’s “Mathematics: Form and Function”, published in 1986, 476 pages. He died in 2005 and never wrote a word about AI, and I haven’t found anyone bringing this book into this year’s debate. So what follows is half the book and half my own reading of it, and I will mark which is which.

Here is my answer up front: machines are finishing off the “form”; the “function” still needs someone to claim it.

Let me set out the facts first, so nobody can say I’m in denial.

A year ago, it was a joke. In October 2025, a vice president at OpenAI tweeted that GPT-5 had found solutions to 10 unsolved Erdős problems. Thomas Bloom, who maintains the Erdős problems website, replied that this was “a dramatic misrepresentation”. A problem marked “open” on the site only meant that he personally didn’t know of a solution. What GPT-5 had found was old literature he had missed. The tweet was deleted, and DeepMind’s Hassabis called the episode embarrassing. (As reported by Futurism and others.)

Seven months later, the joke had become news. On May 20, 2026, an OpenAI model disproved Erdős’s unit distance conjecture. Place n points in the plane: how many pairs of them, at most, can be exactly distance 1 apart? Erdős conjectured that the answer is essentially of order n. The model’s construction has an exponent strictly greater than 1. The mathematician Will Sawin then worked out the number: more than n^1.014 pairs.

Behind it is algebraic number theory: build algebraic number fields of large degree and small discriminant, with the Golod-Shafarevich criterion guaranteeing that they exist. An old problem in combinatorial geometry, cracked open with the tools of number theory.

The same day, nine mathematicians wrote up an account of it: short, digested, checked by hand. The authors included Gowers, and also Bloom, the same Bloom who had corrected OpenAI the year before.

Over the next few weeks, one result followed another. The Jacobian conjecture, posed in 1939, got a counterexample in three complex variables, found by Alpöge with the help of AI; you don’t have to trust anyone, because you can check it by direct computation. Sendov’s conjecture got a proof from AI, which Tao then simplified so that it uses only basic complex analysis and the Maclaurin inequality. On September 4 came the news that an Anthropic model had spent 11 days translating the entire proof of Fermat’s Last Theorem into Lean. Kevin Buzzard, who is doing the same thing himself, titled his blog post “FLT: Anthropic has beaten me to it”.

In the first week of October, things came even faster.

On October 4, the KLS conjecture got a complete proof. It is a central problem of high-dimensional geometry, open since 1995: every isotropic log-concave distribution has a Cheeger constant bounded below by a positive constant that does not depend on the dimension. Zhao Song and Xinzhi Zhang improved the O(4^{log* n}) bound they had posted on October 1 to O(1). On the same day, Bizeul, Klartag and Lehec posted another proof, with Song and Zhang’s criterion as a key step.

Both papers explain in their acknowledgments how AI was used. Song and Zhang list the four models they used and say that from July 28 onward they explored more than a hundred approaches together with AI tools, with the humans deciding which to try first. Bizeul, Klartag and Lehec are blunter: most of the proofs and mathematical ideas were found by ChatGPT, and only the idea of suspension came from the authors; the authors’ role was mainly to understand these proofs and to improve the writing.

On October 5, Josh Alman and Virginia Vassilevska Williams posted a paper: a deterministic O(n^1.9992) algorithm for 3SUM, and an O(n^2.9995) algorithm for APSP. The paper says this refutes the 3SUM hypothesis and the APSP hypothesis, two cornerstones that fine-grained complexity has rested on for decades.

The paper’s preface says one more thing: the algorithm was discovered by Claude. An Anthropic employee was using an internal research model on an open problem in cryptography, asking it to verify and improve a construction, and the model went off on its own and found this algorithm instead, first for the average case, then for the worst case. The whole session used 16 million output tokens, with no human input. In September, Anthropic handed it to the two authors under a non-disclosure agreement. The authors then worked to understand it, simplify it and strengthen it, and the main results were also verified by Claude in Lean 4. The authors state that they take full responsibility for the paper. Both papers have only just been posted and have not yet been peer-reviewed.

It does slip up, though. First Proof is a set of ten unpublished, research-level problems posed by 11 mathematicians. In the first round (February), the problem-setters’ own grading found about 2 clearly solved; the companies claimed 5 or 6, and the argument is over how much human help went into the ones in between. (As reported by Scientific American.) The September 8 episode was OpenAI’s announcement that it had constructed a finite-time blowup for the Navier-Stokes equations with a smooth forcing term, which I wrote about earlier. As of today, there is no independently verified conclusion.

To be fair: a year ago, most news like this could be read as marketing. Not anymore. The verification of the unit distance result was written by people like Gowers and Bloom, who are about as hard to fool as anyone, and they wrote it themselves.

So I won’t spend any ink on whether AI is up to it. Tao’s ICM lecture this year likewise begins by saying he won’t discuss this: he simply assumes these capabilities will arrive, and turns to a different question, namely what the goals and values of mathematical research really are.

Read through this month’s essays and posts and you will find that people are not arguing about whether AI is up to it. They are arguing about what mathematics actually produces.

Buzzard’s October 1 post states its position most plainly. The total number of theorems, he says, is what he went into mathematics for. Mathematics is infinite, more than even exponential growth could ever exhaust, so if AI finds more theorems, that is a good thing. He doesn’t buy Thurston’s view. In a famous 1994 essay Thurston argued, roughly, that mathematicians are not meeting a production quota of theorems and proofs; success is measured by whether people come to think more clearly as a result. Tao’s ICM lecture quotes it again. Buzzard also wants the companies to make public the proofs they are holding; humans will come to understand them in time.

On September 11, an open letter, initially signed by 25 Fields medalists, appeared under the title A Severe Misalignment of AI in Mathematics. Its core sentence: solving problems is only a tool for, and only a proxy for, the primary goal of conceptual understanding. When companies rush out announcements without writing the work up, putting their names to it or explaining it, the chain by which people hand mathematics down is broken. The letter does not call for banning anyone; it calls for dialogue.

Gowers did not sign the letter. He says mathematicians sit along a spectrum, with problem-solving at one end and understanding at the other, and that it is unfair of the letter to rank understanding above problem-solving. What really worries him is something else: whether the people who would have gone on to do PhDs, and one day taken over the craft, will stop coming.

Litt’s view is that mathematics has never been just about saying true sentences; it also includes asking the right questions, being confused, stumbling around. On September 13 he proposed a set of remedies: replace the PhD thesis with an oral defense, and hire on the strength of talks and discussions rather than by counting papers.

Online, the fight is louder still; the comment sections are like a pot of porridge at a rolling boil. On Hacker News the letter got 1,242 points and 1,215 comments. Some said its real target was not AI but companies that only care about headlines; some thought the word “misalignment” too strong; and some drew an analogy with Mochizuki’s proof of the abc conjecture: a proof nobody can follow can also spark a whole wave of research. On Bilibili, a video titled “After AI started brute-forcing hard math problems, why are mathematicians united against it?”, posted on September 18, has about 290,000 views and 2,011 comments.

Line these voices up along a single axis:

In fact, nobody at either end denies that AI can do real work. The real disagreement is this: what is the function of mathematics? Is it to produce a stock of verifiable true statements, or to help people understand the world more clearly?

That is exactly the question Mac Lane asked forty years ago.

Saunders Mac Lane (1909–2005) wrote the founding paper of category theory with Samuel Eilenberg in 1945, served as president of the American Mathematical Society, and received the National Medal of Science in 1989. He defended his doctoral thesis in Göttingen in 1933; its title translates as “Abbreviated Proofs in the Logical Calculus”. His advisor was Paul Bernays, and Weyl was one of his examiners.

A man whose doctoral thesis was about shortening proofs wrote a book late in life asking what mathematics really is. In 1986 he published “Mathematics: Form and Function” (Springer). It is not a treatise on philosophy; most of its twelve chapters are about mathematics itself: whole numbers and rational numbers, geometry, real numbers, functions and groups, calculus, linear algebra, space, mechanics, complex analysis and topology, and sets, logic and categories. The last chapter is called “The Mathematical Network”.

In the introduction he first explains what the book sets out to do, and then asks:

To answer it, he goes on, we must first look closely at mathematics: a philosophy of mathematics that does not rest on an examination of mathematics itself is not convincing. He even names names, saying that Wittgenstein and other philosophers failed on exactly this point.

A sketch of his answer appears in a 1981 article (“Mathematical Models: A Sketch for the Philosophy of Mathematics”, Amer. Math. Monthly 88). The 1986 book follows the same line of thought and gives a longer table in Chapter I, §I.11.

Mathematics comes from human activities. The 1981 article lists ten:

One item on the list deserves a second look: proving. For him, proving is one of ten human activities, and it leads to logic. It is a part of mathematics, not the whole of it.

What the activities leave behind are vague ideas, such as “next”, “symmetry” and “approximation” (examples from the table in Chapter I). The work of mathematics is to peel off the part of these ideas that is general and not arbitrary, formalize it, and write it down as axioms, definitions and theorems. Then the form goes back into the activities and helps people see them clearly. One sentence of his sums it up: mathematics is formal, but not merely “formalist”, because its forms come from human activities and are used to understand those activities.

He is blunt with all the main schools. Logicism, formalism, intuitionism, Platonism, empiricism: none of them, he says, gives a satisfactory analysis. Identifying mathematics with whatever can be derived in set theory he calls “one-sided”: set theory is largely irrelevant to the practice of most mathematics, and it cannot explain why mathematics works so well in science.

He calls foundations proposals for organizing mathematics, not the ground it stands on. Mathematics is not a pyramid built on one set of axioms; it is a network.

“Form comes from activity and goes back to it.” Can we put that more sharply? Let’s run an experiment on the oldest of the ten activities: counting.

The idea counting leaves behind is “next”. Formalize it and you get the Peano axioms: there is a starting point 0; every number has a unique successor, written S; 0 is not the successor of any number; different numbers have different successors; and, finally, an axiom of induction. The question is: do these axioms pin “counting” down completely? There are two answers, pointing in opposite directions.

The two theorems below come with proofs. Skip the proofs if you like, but not the statements or the figure.

In other words: as long as you are willing to talk about “arbitrary subsets”, counting is pinned down completely. There is only one sequence of natural numbers in the world, whatever material you build it from.

But first-order logic only lets you write one induction axiom for each formula (an “axiom schema”); it cannot talk about “arbitrary subsets”.

Put the two theorems together and you get a small trade-off. To lock down the meaning of “counting”, you need a language that can talk about “all subsets”, and that kind of second-order logic (with full semantics) has no mechanical proof calculus that is both sound and complete (a consequence of Gödel’s incompleteness theorem). The first-order language, whose consequences a machine can work through exhaustively, cannot lock it down. Pinned down uniquely, or mechanically exhaustible: you cannot have both.

Today’s proof assistants use stronger type theories with the natural numbers built in, but the trade-off does not go away. What the machine checks is the formal statement you wrote down; whether that is the question you really meant to ask, no system can vouch for you. That is what I meant before when I said someone has to read Lean files word by word.

In the same article Mac Lane distinguishes two kinds of structure. The natural numbers, the rationals, the reals and Euclidean geometry are meant to be unique; groups, rings and topological spaces are meant from the start to have many models. Counting belongs to the first kind, which is why Theorem 1 matters for it.

He also wrote something to the effect that axiom systems encode deeper, non-obvious properties of the activity. The two theorems read like a precise version of that remark: how much of an activity a form can capture depends on what price you are willing to pay; and whether it has actually done so can only be judged by going back to the activity itself. (That last clause is my own reading.)

Tao’s ICM lecture includes a piece of history. Russell’s paradox came in 1901 and Gödel’s incompleteness theorems in 1931; between 1900 and 1930, mathematics went through a crisis in its foundations. What came out of the crisis was an explicit, standardized foundational framework: the objects of mathematics and the rules of reasoning were laid out in the open, where they could be checked and taught, and where, later on, proofs could even be mechanized.

We have now entered, he goes on, a period of comparable upheaval. The difference is that what is being stress-tested this time is not the foundations of truth but the implicit framework of values and conventions: what counts as a contribution, what gets rewarded, what counts as understanding, and who, or what, did the work.

In Mac Lane’s terms: the last crisis was a fight about form. This one is about function.

Mac Lane’s standard for form, as it happens, already anticipated today. On page 377 of the book he says that a mathematical proof is rigorous when it is (or could be) written out as a formal proof in the first-order predicate language; a proof in practice is a sketch, detailed enough that it could be routinely translated into a formal proof.

In 2026, “routine translation” became genuinely routine. In September, an Anthropic model spent 11 days translating the whole proof of Fermat’s Last Theorem into about 13.4 million lines of Lean. Buzzard, one of the standard-bearers of the formalization camp, said he was 99.9% sure the proof was fine, and that the formalization simply followed the earlier literature faithfully, without adding anything new. Rather like spending 11 days making a fresh copy of a book everyone already believed. His own FLT project is after something else: a living document that people can explore.

Rigor was bought; not one ounce of understanding came with it. In Section 9 of the 1981 article, Mac Lane had already said that rigor is not enough. A balanced philosophy of mathematics, he wrote, must add three things to rigor: breadth, clarity and depth. Clarity is precision beyond rigor, a clear ordering of ideas. Depth is grasping the non-obvious, more fundamental structure underneath a problem, the way group theory underlies symmetry.

Nearly every new buzzword in mathematics this year finds a place among these three. When Tao says AI-polished proofs are easy to read but hard to learn from, that is a problem of clarity. What he calls digestion and canonization are breadth and depth.

Mac Lane himself carried out one of the most beautiful “digestions” there is. In 1963, in “Natural associativity and commutativity”, he took up tensor categories. There, associativity (A⊗B)⊗C ≅ A⊗(B⊗C) is not an equality, only an isomorphism. A product of four objects can be bracketed in 5 ways; of five, in 14 ways; of six, 42; of seven, 132. Any two bracketings can be joined by associativity isomorphisms, but do different ways of joining them give the same result? That is infinitely many questions.

Infinitely many checks, compressed into one. That is digestion. This July, Tao broke the Jacobian counterexample down into three properties and explained each in turn; in August, he simplified the Sendov proof until it used only basic complex analysis. He was doing the same kind of thing, just without a theorem named after it.

Tao went through five drafts of the goal of “solving a problem”. The final version: solve an open problem, verify the solution, explain it clearly, and have the community digest it, accept it and fold it into the field’s canon. He lays the whole process out in five stages: producing, verifying, explaining, publishing and digesting.

AI has already taken over the first two boxes and is moving into the third. The fourth and fifth are the slowest stretch and, Tao says, also the most valuable. He makes another observation too: AI’s ability to do mathematics at all rests on the standard theory that humans have rewritten again and again over the centuries. The training data, put plainly, is the product of canonization.

Another of his judgments cuts deeper: we are moving from a “scarcity of proofs” to a “glut of proofs”. Journals, priority conventions, hiring and promotion criteria, prizes, even the very idea of a “research program”, were all designed on the assumption of scarcity. In a glut, they start to warp.

None of these changes is an argument about whether AI is up to it. Each of them asks the same thing: what function was this institution meant to serve in the first place?

Mac Lane would not have been surprised. His view was that foundations are only proposals for organizing mathematics, and that as mathematics grows the proposals have to change. A fixed foundation would shut out the discovery of new forms. (Following McLarty’s review of the book.)

Back to the title. What follows is my own extrapolation from Mac Lane’s framework, not his conclusion, in three points.

First, Buzzard’s rebuttal holds up. Mathematics is infinite, the number of theorems is something real and measurable, and “understanding” is a word nobody can pin down. Besides, Mac Lane was not purely human-centered either. His 1981 definition of mathematics was the discovery of the formal structures that underlie the world and human activities in it, built up layer upon layer. The word “world” is right there.

Second, his ten activities are bodily and ancient: counting, measuring, moving, shaping. Today’s algebraic geometry is a long way from them. His answer is to build ideas on ideas, layer upon layer. But whether AI can stack form upon form by itself, without any new human activity, is a question the book does not answer. The preface of the Alman paper is a ready-made case: the model veered off into this algorithm on its own while working on a task someone else had set, with no human input. The problem came from a person; the path was walked by the machine.

Third, philosophers do not agree on how to read him. McLarty sees him as a model naturalist philosopher; in 2025, Skowron argued in Philosophia Mathematica that his “ideas” are in fact close to ideal entities, at odds with his stated opposition to Platonism.

Back to those six days at the start. arXiv is capping submissions, Bloom is freezing his site, Córdoba says he can’t comment for now, Buzzard is staking out a position somewhere between grief and optimism. The authors of the KLS and 3SUM papers describe their roles in their acknowledgments in much the same words: understand, simplify, improve the writing. Everyone is looking for a new function for one of the “forms” in their hands: the paper, the problem list, the PhD thesis, the conference.

Tao says we need to spell out the goals that have never been written down. That is a writing task. Mac Lane took it on once, in 1986: rather than wait for the philosophers, he walked through mathematics from the beginning himself, then turned around and asked what all of it is for.

AI is getting better and better at the activity of “proving”. But proving is only one of the ten on his list.

“Form can be handed to the machines;
function still needs someone to claim it.

If one day machines grow new “activities” of their own and stack ideas on them by themselves, that will be a question for another book.