Why Math Dumped OpenAI

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.

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 don’t like LLMs, the Liar’s Layoff Machine.

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

— Liz Martinez, co-host of The Coding Agency

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.

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

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.

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

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.

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.

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.

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

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.

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.

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

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

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.

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.

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.

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:

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.

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.

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.

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.

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.

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

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