别让任何人把数学家称作卢德分子。不。

数学领域的 AI 原本具有天然协同效应，研究者也曾_竭尽全力_地拥抱它。OpenAI 却把这种关系变成了一段有毒关系。这场信任崩塌与我们在软件工程和其他领域所看到的情况并行发生。

当程序员说数学家如今也在“感受我们的痛苦”时，有些人的意思是：数学家震惊地发现机器已经超越了他们。如果你只看过近期新闻、不了解此前的背景，这种理解虽然天真，却也可以理解。下面我会解释。

实话实说

OpenAI 在数学前沿的定位，并不是贡献最大的参与者，而是预算最高、嗓门最大、诚信最差的参与者。

人们把 ChatGPT 称为“超级智能”，却不认为 Lean 证明器是超级智能，原因在于 Sam Altman 是个骗子，而 Leonardo de Moura 不是。

Lean FRO 对这些同类突破所作的基础性贡献更加诚实，也_更具影响力_，而其资源还不到 OpenAI 的 1%。这还只是我们可以说“机器”正在“做”的那一部分；通常我们会把它表述为，研究结果被形式化或机械化。

有人可能会认为，统计语言引擎天生就不如 Lean 这类符号系统诚实，但实际上二者相互补充。这并不是问题所在。问题在于，数十亿美元正被投入一场系统性去人化、贬低劳动者价值的运动。

我喜欢 LLM，也就是大型语言模型。

我不喜欢 LLM，也就是骗子裁员机器（Liar’s Layoff Machine）。

你永远都不够好

这不是一个从敌人变成恋人的故事。这是一个从恋人变成敌人的故事。

—— Liz Martinez，The Coding Agency 联合主持人

不存在“拥抱 AI”的办法。

这是一段与施害者之间的有毒关系。要求受害的一方“拥抱变化”解决不了任何问题。如今 AI 鼓吹者遭到敌意，是因为他们共谋参与了煤气灯操控。

我也曾是早期采用者。这就是它最终会走向的地方。你可以付出一切努力，但永远不会足够，因为它不是为你而造的。

诊断

我想说的是，AI 淘金热展现出了自恋型施虐者的模式。

我知道你在想什么：

Ray，自恋与那些建立在某种不可避免、神一般且超级智能的公司，到底能有什么关系？这种智能又如此危险，以至于不能相信其他任何人来创造它，并且理应成为我们全球规划的核心焦点？

问得好。暂时我们只能把这留作读者练习。今天的文章是一项纵向案例研究。

我不是医疗专业人士，而且医疗专业人士也不会诊断淘金热；但按照 DSM-5 标准，要诊断为自恋型人格障碍，需要具备下列 9 项特征中的 5 项或以上。

1. 夸大的自我重要感
2. 经常幻想拥有或理应获得：
   • 成功
   • 权力
   • 智力
   • 美貌
   • 爱
   • 自我实现
3. 相信自己优于他人
4. 需要他人赞美
5. 权利感
6. 愿意利用他人
7. 缺乏同理心
8. 经常嫉妒
9. 傲慢

其中有任何一点听起来耳熟吗？

飞猴

飞猴是指受自恋者影响、替其行事的人，他们会：

• 散布谎言和流言蜚语
• 共同构建幻想
• 通过辩护、淡化或找借口，纵容虐待行为

在这个类比中，AI 鼓吹者就是飞猴。他们或许本意良善，也困惑于人们为何会对他们坚持要求大家与施害者和解作出如此反应——而这再说一次，是不可能的。他们想知道，这些反 AI 的人为什么变得如此刻薄。

DARVO 是 Deny（否认）、Attack（攻击）和 Reverse Victim and Offender（颠倒受害者与施害者）的首字母缩写。

Olivia Guest 教授在这里解释了一个 DARVO 的案例。她采用的批判性 AI 素养方法经常引来这类攻击。这是一场不对等的游戏：机器学习专家在其他所有人的领域里——例如认知科学——反而更容易被认真对待。

反应性虐待指的是故意触发对方反应，从而将受害者归咎为施加攻击的一方，并让他们看上去才是问题所在。

另一个与此相配的策略是，无论我们多少次解释自己是在批评特定的_人_及其_行为_，都假装冲突的对象字面上是机器本身。

现在不行，Dario，我们正试图严肃一点。

边界

又一群领域专家正在经历与美国模型实验室之间的信任崩塌。

利益相关者已经明确表达了自己的需求：情况必须改变。在多次更温和的尝试失败后，他们正在设立边界。

这是一个关于 AI 在数学领域最伟大的盟友如何最终开始宣传这些公开信——并签署第一封——的故事。

无论飞猴们如何歪曲，这些人都不是仅仅害怕变化或自动化的人。他们支持更好的改变，批评更坏的改变，并且清楚解释了二者的区别。

接下来的文章将按照我追踪这些事件时的顺序，梳理导致这一结果的过程。希望这对你有所帮助。

第一幕：铺垫

我们的主角

这位是 Terence Tao，被认为是当代最伟大的数学家。在过去十年中，他也成为数学数字化进程中的文化领袖。我们将在这条时间线中主要跟随他。他是其所代表群体可信的发言人。

2014 年 11 月

上图中的他拍摄于 2014 年。那一年，他说：

有一天，我们或许不会再用 LaTeX 写论文，而会使用某种语言，某个智能软件会将其转换为形式化语言；并且每隔一段时间，你会遇到一次编译错误——计算机不理解你是如何推导出这一步的。

—— Terence Tao

尽管当时已经有能够做到这一点的编程语言，例如 Isabelle，但它们被认为晦涩且难以使用。Tao 预见到它们可能会在职业数学家中流行起来，这种看法极具前瞻性。

如今，当我们谈论高级层面的“AI 做数学”时，最常见的配置是：一个基于 LLM 的 Agent 驱动传统证明助手（Lean），并建立在经过整理、已有形式化结果组成的库（Mathlib）之上。

想了解更多，可阅读 Kevin Hartnett 撰写的文章《Terry Tao 如何成为数学 AI 的布道者》，或他关于 Lean 证明器诞生的新书《代码中的证明》。强烈推荐。

2019 年 10 月

我第一次听说 Lean，是在 Kevin Buzzard 2019 年的演讲《数学的未来？》中。他属于一个不断壮大的数学家群体，支持采用证明助手来形式化数学结果。

他指出了一个关键挑战：要让这个领域感到兴奋，我们必须能够形式化_新的结果_。新结果依赖许多尚未形式化的旧结果——这是一个经典的自举问题。他用费马大定理来说明这一点。它是数论结果事实上的“最终 Boss”；Andrew Wiles 在 1995 年著名地证明了它，而此前它因需要尚未被发明的思想而悬而未决长达_300 年_。将费马大定理的证明形式化非常_困难_。

给我 1 亿美元和 10 年时间，我相信可以组建一个团队来形式化费马大定理的证明。我认识的数学家中，没有人对此表示异议。

目前成本高得令人望而却步。

但更糟的是，没有真正的数学家会在意这件事［因为它是一个已经被接受的旧证明］。

—— Kevin Buzzard，2019 年

后来他最终获得了 100 万美元和 5 年时间，这已经相当不错了！我们稍后会回到这件事。

2023 年：基础 LLM 升级

2023 年 3 月，为回应 OpenAI 发布 GPT-4，我写下了《机械化修补宣言》（Mechanized Mending Manifesto），试图建立一个模型，说明这些创新与我们在工业软件中面临的挑战有何关联。显然_某些事情_已经改变了，但究竟是什么？我鼓励人们以三个要素而非此前两个要素来思考系统。

• LLM
• 传统算法
• 人

这是对“大型语言模型可以直接替代人类或算法”这一观点的反叙事。它们各自有不同的优势和弱点；若要构建优秀系统，我们需要理解这些差异。当时我还不理解，既得利益者正试图让 LLM _看起来_比实际更接近人类等价物，其力量有多么庞大。这是我的天真之处。

我开始寻找能够发挥各要素优势的平衡系统，希望借此指明方向。

2023 年 10 月：Tao 采用 Lean

那年晚些时候，我在社交媒体上看到了这句意义重大的话。

Terence Tao 正在使用 ChatGPT 学习 Lean 证明器。

了解背景的人知道，这可能意义重大。如果顶尖数学家采用 Lean 证明器，正如 Buzzard 所预测的，它可能塑造数学的未来。Tao 的领导力可能成为产生决定性影响的推动力。ChatGPT 有助于降低使用门槛，而 Lean 则能控制众所周知的 LLM 幻觉问题。

这正是我的宣言所设想的和谐范例：LLM、算法和人类共同协作，发挥各自优势。

自然数游戏仍是开始学习 Lean 的最佳方式，而且它现在的自文档化程度更高；如果你愿意，应该不需要 ChatBot 也能学好。参见我的文章《如何学习定理证明器》。

2024 年：我孤独的可靠性之路

受 Hillel Wayne 和 Marianne Bellotti 启发，我宣布 2024 年为形式化方法之年。我学习了许多证明器，经历了许多头痛，也制作了许多视频。

为了从 LLM 获得最佳结果，我们需要理解它们的弱点。不幸的是，我经常发现，人们对“LLM 有弱点”这件事变得极其敏感，因为他们正试图推销淘金热的宣言：拥抱 AI，否则就会被抛在后面。那些试图让 LLM 真正发挥作用的人，持续被指责没有跟上潮流。

在 ChatGPT 发布不到一年后，我为平衡解决方案发声的尝试，使我与“AI 优先”的商业世界严重疏离，以至于我“收回”了卢德分子这个词，并发誓要把它当作一种褒奖和志向。

对我来说，以有益的含义成为卢德分子，并不意味着反对所有新技术，而是专门反对在以下情形下引入技术：

• 具有欺骗性
• 降低产品质量
• 恶化工作条件

把你的鞋扔进齿轮里。

第二幕：破坏

2025 年 2 月

GPT-4 发布两年后，OpenAI 联合创始人、世界首富 Elon Musk 开始将 AI 作为烟幕，削弱美国政府职能。这项行动被称为 DOGE，名称取自一种加密货币骗局，是“政府效率部”（Department of Government Efficiency）的缩写。尽管这是美国历史上规模最大的联邦雇员裁减行动，支出却没有下降。

这导致了死亡和其他伤害。

2025 年 7 月

DOGE 的受害对象包括由美国国家科学基金会资助的数学研究经费。

作为规模参照，NSF 的全年总预算约为 80 亿美元。OpenAI 在 2025 年筹集了 400 亿美元风险投资，并在 2026 年筹集了 1220 亿美元。

2025 年末

Terence Tao 继续在自己的博客和 YouTube 视频中教其他数学家使用形式化方法，采用 Lean 证明器以及 ChatGPT 和 Claude Code。他还协调了大规模协作工作。他就 AI 在数学和科学中的潜力进行了许多演讲和访谈。

他已经尽可能地“站队”支持了。不过，在这张照片里他似乎没那么开心。

2026 年 4 月至 5 月

随着我们已经优化，Tao 指出了其中的陷阱

Don’t let anyone call the mathematicians Luddites. No.

AI in Math had a natural synergy that researchers made every effort to embrace. OpenAI turned this into a toxic relationship. This breakdown in trust runs parallel to what we see in Software Engineering and other domains.

When programmers say mathematicians are “feeling our pain” now, some mean it in the sense of being shocked to discover machines have surpassed them. That’s a naive but understandable take if you’ve seen recent headlines without prior knowledge of the situation. I’ll explain.

Calling a Spade a Spade

OpenAI’s position at the frontier of Mathematics is not that of the player making the biggest contribution, but of the player with the highest budget, biggest mouth, and least integrity.

The reason people call ChatGPT a “Super Intelligence,” but don’t consider Lean prover one, is that Sam Altman is a liar and Leonardo de Moura is not.

Lean FRO’s foundational contribution to these same breakthroughs has been more honest and more impactful , with a fraction of 1% of OpenAI’s resources. That’s just speaking of the part we could say “machines” are “doing,” which we normally speak of as results being formalized or mechanized.

One could argue that a statistical language engine is an inherently less honest technology than symbolic systems like Lean, but really they are mutually complementary. That’s not the problem. The problem is the billions of dollars being poured into a campaign to systematically dehumanize and devalue workers.

I like LLMs, the Large Language Models.

I don’t like LLMs, the Liar’s Layoff Machine.

You’re Never Enough

This is not an enemies-to-lovers story. This is a lovers-to-enemies story.

— Liz Martinez, co-host of The Coding Agency

There is no way to embrace AI.

This is a toxic relationship with an aggressor. Asking the aggrieved to “embrace change” will solve nothing. The reason AI Boosters are now met with hostility is because they are complicit in gaslighting.

I was an early adopter too. This is where it ends up. You can make every effort and it will never be enough, because it is not made for you.

Diagnosis

What I’m saying is that the AI Gold Rush exhibits the patterns of a narcissistic abuser.

I know what you’re wondering:

Ray , what could narcissism possibly have to do with companies founded on an inevitable God-like Super Intelligence so dangerous that no one else can be entrusted to create it, which should be the central focus of our global planning?

Good question. We’ll have to leave that as an exercise to the reader for now. Today’s post is a longitudinal case-study.

I’m not a medical professional and they don’t diagnose gold rushes, but under the DSM-5 criteria, the diagnosis of Narcissistic Personality Disorder requires 5 or more of these 9 traits.

1. Grandiose sense of self-importance
2. Frequent fantasies about having or deserving:
   • Success
   • Power
   • Intelligence
   • Beauty
   • Love
   • Self-fulfillment
3. Belief in superiority
4. Need for admiration
5. Entitlement
6. Willingness to exploit others
7. Lack of empathy
8. Frequent envy
9. Arrogance

Does any of this sound familiar?

Flying Monkeys

Flying Monkeys are people under the influence of narcissists that act on their behalf by:

• Spreading lies and gossip
• Forming a shared fantasy
• Enabling abusive behavior by defending, dismissing, or excusing it

In this analogy, AI Boosters are Flying Monkeys. They might mean well, and are confused at how people react to their insistence that we make peace with the abuser (which, again, is impossible). They wonder how these Anti-AI people got so mean.

DARVO is an acronym for Deny, Attack, and Reverse Victim and Offender.

Professor Olivia Guest explains a DARVO example here. Her approach to critical AI literacy frequently draws this kind of attack. It’s a lopsided game where Machine Learning experts are taken more seriously about everyone else’s field, e.g. Cognitive Science.

Reactive abuse is intentionally triggering a reaction in order to blame the victim for aggression and make them seem like the problem.

Another tactic that pairs well here is to act like the conflict is literally with the machines no matter how many times we explain that we are criticizing specific people for their actions.

Not now, Dario, we’re trying to be serious.

Boundaries

Yet another group of domain experts is experiencing a trust breakdown with the US model labs.

The constituents are making their needs clear that things need to change. They are setting boundaries after numerous softer attempts failed.

This is the story of how the greatest ally of AI in Math wound up promoting these letters (signing the first).

No matter how the Flying Monkeys try to spin this, these are not people who merely fear change or automation. They are people supporting change for the better, criticizing change for the worse, and clearly explaining the difference.

The rest of this post will outline events that led to this as I followed them. I hope you find it helpful.

Act I - Setup

Our Hero

This is Terence Tao, considered the greatest living mathematician. Over the past decade he has also become a cultural leader in the digitization of Mathematics. We will mostly follow him in this timeline. He is a credible spokesperson for their constituency.

November 2014

He’s pictured above in 2014, the year he said:

One day we may actually write our papers not in LaTeX, but in some language which some smart software will convert to a formal language, and every so often you’ll get a compilation error — the computer does not understand how you derived this step

— Terence Tao

Although there were already programming languages capable of doing this, such as Isabelle, they were considered obscure and hard to use. Tao was being extremely progressive in anticipating they could catch on for working mathematicians.

Today, when we speak of “AI doing Math” at advanced levels, the most common setup is an LLM-based agent driving a traditional proof assistant (Lean) building on a curated library of already formalized results (Mathlib).

For more, see How Terry Tao Became an Evangelist for AI in Math article by Kevin Hartnett or his new book The Proof in the Code about the creation of Lean prover. Highly recommended.

October 2019

I first heard of Lean in this 2019 Kevin Buzzard talk: “The Future of Mathematics?”. He was part of a growing group of Mathematicians supporting the adoption of proof assistants to formalize the results.

He called out a key challenge: to become exciting to the field, we needed to be able to formalize new results. They depend on many old results, not yet formalized — a classic bootstrapping problem. He illustrated this on Fermat’s Last Theorem , the de facto “final boss” of Number Theory results, which Andrew Wiles famously proved in 1995 after it went unsolved for 300 years because it required ideas not yet invented. Formalizing the FLT proof is hard.

Give me 100 million dollars and 10 years and I believe I could get a team together to formalize a proof of Fermat’s Last Theorem. No Mathematician I have met disputes this.

Currently prohibitively expensive.

But worse, no proper mathematician would care [because it’s an old accepted proof].

— Kevin Buzzard, 2019

He eventually got 1M and 5 years, which is something! We’ll come back to that.

2023 - Foundation LLMs Level Up

In March 2023, in response OpenAI’s release of GPT-4, I wrote the Mechanized Mending Manifesto to model how these innovations relate to our challenges in industrial software. It was clear something had changed, but what? I encouraged thinking of systems in three elements where there were two before.

• LLMs
• Conventional Algorithms
• People

This was a counter-narrative to the idea that Large Language Models are a direct replacement for people or algorithms. These each have different strengths and weaknesses that we need to understand to build good systems. I did not yet understand that magnitude of the vested interests trying to making LLMs appear more human-equivalent than they actually were. That was naive of me.

I began looking for balanced systems that leveraged the strengths of each element, to show the way.

October 2023 - Tao adopts Lean

Later that year I saw these momentous words on social media.

Terence Tao is using ChatGPT to learn Lean prover.

People with context knew this could be huge. If top mathematicians adopted Lean prover it could shape the future of mathematics, as Buzzard predicted. Tao’s leadership could be the push that made the difference. ChatGPT helped reduce the friction while Lean controlled for the notorious LLM-hallucinations.

This was a perfect example of the harmony my manifesto suggested: LLMs, algorithms, and people working together to leverage strengths of each.

The Natural Number Game is still the best way to start learning Lean, and it’s now more self-documenting so you should be fine without a ChatBot if you prefer. See my post How To Learn Theorem Provers.

2024 - My Lonely Road To Reliability

I declared 2024 The Year of Formal Methods, inspired by Hillel Wayne and Marianne Bellotti. I learned many provers, had many headaches, and made many videos.

To get the best results from LLMs, we need to understand their weaknesses. Unfortunately, I often found people became extremely touchy about LLMs having weaknesses, because they were trying to push the Gold Rush’s manifesto: Embrace AI or be Left Behind. People trying to make LLMs actually work were constantly accused of failing to get on board.

Within a year of ChatGPT’s release, my attempts to advocate balanced solutions had left me so alienated from the “AI-first” business world that I “took back” the term Luddite and vowed to take it as complement and an aspiration.

To me, being a Luddite in the useful sense would not mean we oppose new technology in general, but specifically oppose its introduction when it’s:

• Deceptive
• Degrades product quality
• Degrades work conditions

Throw your shoes in the gears.

Act II - Sabotage

February 2025

Two years after GPT-4, co-founder of OpenAI and world’s richest man Elon Musk began using AI as a smoke screen to gut functions of the US government. This effort was called DOGE, named after a crypto-currency scam, and short for “Department of Government Efficiency”. Despite the largest ever federal workforce cut in history, spending did not go down.

This resulted in deaths and other harms.

July 2025

Casualties of DOGE included Mathematics research funding by the National Science Foundation.

For scale, the entire annual budget of NSF is roughly $8 billion USD. OpenAI raised $40 billion of venture capital in 2025 and $122 billion in 2026.

Late 2025

Terence Tao continued teaching other Mathematicians his formalization methods on his blogs and YouTube videos, using Lean prover along with ChatGPT and Claude Code. He coordinated large collaborative efforts. He gave many talks and interviews about the potential for AI in Math and Science.

He was as “on board” as you could ask anyone to be. Albeit he seems less happy in this picture.

April-May 2026

Tao points out the pitfalls as we have optimized some of the process but not others. He explains this as proof digestion. We were generating proofs without integrating them into our understanding. Most of this increased output was not advancing Math.

Perhaps surprisingly, this massive acceleration in proof generation has not actually produced significant acceleration in mathematical progress itself […]

Just as modern societies no longer consider raw food ingredients as constituting a meal, I predict that mathematical research culture will cease considering “raw”, “undigested” proofs as constituting a solution to a problem, and focus more on how the field as a whole, as opposed to just the problem itself, is enriched by the contribution.

Tao, April 2026 Thread

I have recently made the point that out of three major components of the mathematical problem solving process - proof generation, proof verification, and proof digestion - the first two are being automated far more successfully than the third, leading to a new experience of “proof indigestion” in which proofs are being generated and even verified without being digested.

It has been proposed that the solution to this is simply to automate the third component as well - for instance by training AI to write mathematical proofs at a higher level of exposition. This will help to some extent, especially as AI capabilities continue to improve; but blindly optimizing various metrics for “digestibility”, such as rubrics for mathematical exposition, can make the final product worse when viewed holistically.

— Tao, May 2026 Thread

This would have been a perfect signal for the model labs to pick up on, if they wanted to address the actual needs.

September 2026

Fermat’s Last Theorem

Anthropic announces Formalizing Fermat’s Last Theorem, reconstructing the 1995 Andrew Wiles proof in 13 million lines of Lean code.

This is impressive but not categorically different from what had already been achieved. It’s the last of the top 100 of mathematical theorems to be formalized in a prover. The other 99 had already been done by 2024 with people and provers, without LLMs. However FLT was undoubtedly the hardest, and this accelerates the process.

Remember, Kevin Buzzard explained how to do this years ago, it just wasn’t funded.

Buzzard is a Good Sport

Buzzard responded with “FLT: Anthropic has beaten me to it, explaining what’s been done and what hasn’t. He continues with his own efforts to create a more modern version with reusable modules to advance the long-term goals.

I am currently being funded by the EPSRC to formalize a proof of Fermat’s Last Theorem, and a naive reaction to the news above is that I no longer have any work to do. This is not the case. The work certainly achieves some of the aims of the EPSRC project […] But I also promised several other things to EPSRC: firstly, that I would be making pull requests to Lean’s mathematics library, adding fundamental objects from modern number theory; this is ongoing. And secondly, and perhaps most importantly, that I would be creating a dynamic document enabling humans to explore the modern proof. […] From my understanding of the argument, the formalization just faithfully follows the early literature on the proof and adds nothing.

What this work does tell us, however, is what is possible in the field of autoformalization. If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly. […] The ability to autoformalize hard material will ultimately make the review process for mathematics papers far less painful. It will also keep us honest — there are papers out there which assume results which are “known to the experts” and it will be interesting to see exactly what is being assumed in the proofs of various important results in my field. This is why I am so excited about the news!

— Kevin Buzzard

Navier–Stokes Controversy Ignites The Powder Keg

OK, here we go. This single day event has it’s own Wikipedia page.

On September 8th, OpenAI announced a solution to the Navier–Stokes Millennium Prize Problem. The Millennium Prize Problems are highly prestigious and carry a $1 Million USD prize. OpenAI spent an estimated $15 Million in tokens on the effort.

Mathematicians Tristan Buckmaster (New York University) and Levent Alpöge (Anthropic) were independently near a solution building on work by Diego Córdoba and Luis Martínez-Zoroa. Buckmaster was in communication with OpenAI before their announcements. After talks broke down, he disclosed his results early, apologizing for the quality because agents don’t do the full job.

Ideally, we would have preferred to spend weeks turning the LLM generated proofs into something readable from the very first page. This level of care is what these problems and the community devoted to these problems deserves. The various Boussinesq and Euler write-ups in particular are much closer to what models produce under human direction than to a paper written by a person. The Euler writeup, in particular, can only be described as AI slop. I am sorry for this. The reasons are below, and they involve our being pressured by outside factors.

— Tristan Buckmaster, Sep 6, 2026 statement

Since Buckmaster’s group used tools from both labs that train on user data, some suspect that OpenAI’s unreleased model was trained on the other group’s prompts. OpenAI initially confirmed this as a possibility but later claimed to have ruled it out.

While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models.

— OpenAI’s archived statement

Following an investigation, we have confirmed that Buckmaster’s Codex prompts over the two months preceding this announcement and paper on September 8, 2026, could not have influenced the system in any way, including through training. The OpenAI internal model used for this result was developed through large-scale reinforcement learning on top of a previously pretrained model.

— OpenAI’s updated statement

Buckmaster also alleged that OpenAI’s Sébastien Bubeck asked for Alpöge’s name to be removed in order to make a joint announcement without crediting Anthropic. If virtually anything quoted from Bubeck is accurate than he’s a serious asshole. We don’t know exactly what happened here. I tend to agree with Harris’s summary:

The AI industry is using prominent mathematicians as extras in a marketing operation masquerading as a drama, and that even the most sophisticated among the mathematicians play their roles, naively imagining that the drama is about them.

— Michael Harris, Professor of Mathematics at Columbia University, article: “If you don’t want me to be nice, then I don’t have to be nice”

Back to the big picture

Priority dispute aside, I think it makes more sense to view these tensions as a blip in the larger breakdown in trust.

These points are undisputed :

• Both groups used a combination of foundation LLMs, agents, Lean prover, and Mathlib.
• Experts can direct that combination to close vast Lean proofs with novel results.
• The process still produces an unreadable mess that must be massaged into clear insights.
• The model labs create spectacle by brute-force, outspending what other researchers have access to.
• The model labs train on the past and present work of mathematicians to achieve these results.

I don’t believe OpenAI directly stole an incomplete Millennium Prize result through their model training on user inputs. I believe they are in an overall campaign of devaluing labor starting from their founding charter around automating “most economically valuable work”.

When OpenAI and news media refer to this as progress done by “the model” or by “AI”, that is selective reporting reinforcing the narrative of devaluing labor and downplaying the more reliable tech made by less predatory organizations.

Warning Shot

The open letter A Severe Misalignment of AI in Mathematics is signed by 25 Fields Medalists including Terence Tao, joined by over 8,000 other academics.

In recent months, the success of AI in solving major mathematical problems has made headlines even outside mathematical circles. But solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding and insight. Forgetting this in the world of AI may turn the tool against the primary goal. Indeed, the mass production at faster and faster pace of “true/false” statements could destroy fertile ground instead of breathing life into new ideas.

Often these solutions are announced in a rush, leaving no time for a proper writeup, the isolation of new methods and ideas, and citing relevant previous work of others. As in all creative professions, this raises severe attribution and plagiarism questions. Moreover, without the willing mathematicians who must take care of their development and integration into the mathematical canon, AI-conceived ideas would never become fully alive and the crucial human transmission chain between mathematicians would be lost.

We are witnessing a general threat to intellectual work, with misalignment between the outcome of the use of AI and its initial purpose.

OpenAI performs taking this seriously and forms an advisory group.

October 2026

The paper Navier-Stokes Lost in Translation by Bastounis et al. demonstrates that OpenAI’s result mistranslated the natural language arguments. We have verified Lean proofs with human-readable explanations that don’t accurately describe them. This supports Tao’s warning that verification and digestion are lagging behind proof generation. Again, the agents are not doing the full job.

On the same day, OpenAI makes a choice between helping advance Mathematics or making more headlines. IMO, they clearly knew that this proof dumping wasn’t what the Fields medalists or their advisory group said would help.

They chose drama. It’s good for the IPO.

The Response Becomes a Resistance

The next day, the recently-formed Association for Human Mathematics issues their first statement. Terence Tao shares it. It’s short, so I’ll include it in full (emphasis mine).

Yesterday, on October 6th, 2026, OpenAI – which is currently defending lawsuits against accusations of illegal plagiarism, copyright infringement, and trademark dilution – released a repository of manuscripts purporting to contain solutions to a number of high-profile problems in mathematics.

Mathematicians did not ask for this work to be done. The Advisory Group on Mathematics and Artificial Intelligence, from whom OpenAI has claimed to derive its legitimacy, opened their initial advisory statement by saying that frontier AI corporations should not test advanced mathematical problems on internal models. In ignoring the central premise of the Advisory Group’s position, OpenAI has indicated total disregard for the norms of scientific research — norms that guarantee that mathematics remains trustworthy, ethically researched, and in the public interest.

Mathematicians have a particular vision of progress that is informed by history and field-specific considerations. We reject OpenAI’s assertion that this release advances our subject , and we urge mathematicians and the public to view the value of this publication model with due skepticism.

Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. We urge mathematicians to discontinue their work with OpenAI and to return to a vision of science that centers human understanding.

— AHM Statement on OpenAI’s October 6 Release of Mathematical Documents

Update : Terence Tao has now shared a selection of peer’s statements and presented his current vision in the Math 2.0 talk. I encourage hearing from them directly.

Act III - Severance

Constituencies

A constituent is someone who has expectations of you.

At times like this, I think of Ana Hevesi’s excellent article Stop Wasting Time on ‘Community’. It’s about taking people seriously as your constituency, building reciprocity, shared goals… great stuff.

Anthropic and OpenAI act like maintaining public trust is some ultra-hard problem that they’re doing their best to navigate, but they willfully ignore the solutions. They don’t want the Math community as a constituency. They want to alienate them to get attention.

Same with Software Engineers. They will lie to us, lie to our bosses, declare the craft dead and leave nothing in it’s place. As we try to pick up the pieces, we will be called Luddites whether we use LLMs or not, because the machine God is fake and solutions have to be real.

”Agency”

If there’s one thing that distances you further from the AI Gold Rush than wanting products that work, it’s valuing human agency.

We’ve seen exactly how math progress can be legitimately accelerated by respecting the agency of the experts and how it’s being hindered by doing the opposite. In that context, this recent quote by the OpenAI CEO is rather ironic.

We believe that the world should accept some bad things happening for the benefits of this technology and people having the agency.

— Sam Altman, October 2026, Politico interview.

As luck would have it, the general public had the same reaction! It might be a reasonable quote if said by someone else. It plays so badly now because of OpenAI’s optics.

We look at bad things really happening, not his hypothetical ones. We know that we value our agency, and we know that he does not. That’s what the culture is feeling. They are not like us.

It is manipulative to say we fear progress , because what they are doing is not progress. It’s harm.

DARVO

Recall the DARVO pattern: Deny, Attack, and Reverse Victim and Offender.

Silicon Valley wants Mathematicians to be seen as Luddites — people that oppose their agenda fear progress. Better yet if they can actually rile some of them up enough to sound that way to normal people.

Why is The Association for Human Mathematics read as “Anti-AI”? They have subgroups that do and don’t use LLMs that are working together to respond to corporate interference. Is that “Anti-AI”? The word “Human” only sounds Anti-AI to us because venture capital made “AI” synonymous with anti-social goals.

Signing Off

OpenAI’s October 6th announcement titled “Sharing AI progress in mathematics” was deceptive and disrespectful in the context of the ongoing situation, which established why the move was counter-productive to progress. They are counting on press coverage to miss the nuances, which is a good bet.

The AHM is calling for the Math community to go no-contact with OpenAI. I find their reasoning impeccable, and fully supported by the previous statements of the credible parties. I’ve tried to gather enough context so that any curious person with common sense could understand why.

If we care about Math progress we could fund Math instead of defunding it — just an idea. They could use some of that money to buy tools that help them, and we’ll see who wants to run an honest business supporting experts who get to choose.

This is not just about Math. The right of refusal is being contested everywhere. Throughout our industries, well-meaning people have heard gossip and drawn whatever conclusion. Plenty of people are just trying to get things done and don’t understand why they’ve walked into a minefield.

These are confusing times.

• Breath
• Listen
• Respect boundaries
• Respect agency

Thank you for reading my fourth epistle.

To be continued onThe Coding Agency podcast.

---

Here are some more cheerful books about the world of Math.