Why Math Dumped OpenAI

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.

• Anthropic bans users from ‘needless abusive or cruel behavior’ towards Claude
• Anthropic Has Been Aggressively Lobbying the Vatican to Consider AI Consciousness

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).

• September 11th, 2026 - A Severe Misalignment of AI in Mathematics signed by 25 Field’s medalists
• October 7th, 2026 - Statement on OpenAI’s October 6 Release of Mathematical Documents by Association for Human Mathematics (AHM)

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 on The Coding Agency podcast.

---

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

• Is Math Real?: How Simple Questions Lead Us to Mathematics’ Deepest Truths by Eugenia Cheng
• The Proof in the Code by Kevin Hartnett
• Mathematica: A Secret World of Intuition and Curiosity by David Bessis
• Logicomix: An Epic Search for Truth by Apostolos Doxiadis and Christos Papadimitriou