AI has found a flaw in a major physics paper for first time

A computer language created to spot errors in mathematical theorems has uncovered a fundamental error in a widely cited physics paper for the first time. The researcher behind the discovery says it is the first physics paper he has analysed in this way, which raises a worrying question: how many more contain mistakes?

Specialised software is increasingly used to help mathematicians check their proofs are correct and free of contradictions and logical holes, using a process known as formalisation. The approach has even been proffered as a potential solution to some of the thorniest problems in mathematics, such as Shinichi Mochizuki’s sprawling, 500-page proof for the ABC conjecture, which experts have quibbled over for years.

Now, Joseph Tooby-Smith at the University of Bath, UK, has turned a formalisation language called Lean towards the field of physics. He attempted to formalise research published in 2006 on the stability of the two Higgs doublet model (2HDM) potential, which has been widely cited in the years since, but accidentally revealed an error that undermines the theorem.

Formalised theorems can be used as building blocks to formalise more complex theorems, and Tooby-Smith says that his work was supposed to be a “tick box exercise” to add the paper to a larger project of formalised physics research called PhysLib, modelled on an established database for mathematics called MathsLib. “We’re not going out there to disprove papers; we’re going out there to build results that everyone can use,” says Tooby-Smith.

The Future and Deep Future of AI 2040, a keynote by futurist Matthew Griffin

“The error relates to a statement in which the original authors say that a certain condition, C, is sufficient for a stable solution to the problem. But Tooby-Smith showed during formalisation that there is a condition C that doesn’t provide a stable solution.

Tooby-Smith says that the discovery of the error has a dramatic effect on the paper, but is unlikely to cause problems downstream in work that has built on it and cited it. However, he now fears that many physics papers harbour similar mistakes, but isn’t certain how wide-ranging the problem might be. He thinks this makes a strong case for formalisation to become a standard part of publishing new research.

Tooby-Smith says that physicists tend not to give as much explicit detail in theorems as mathematicians.

“Because a lot of physicists aren’t interested in these nitty-gritty details, sometimes they miss them, and that’s where you get an error,” he says.

Kevin Buzzard at Imperial College London says that formalisation is having a big impact on mathematics, and that there is no reason that theoretical physics, at least, can’t be treated in the same way.

“We tried to do maths like this, and it turned out to be really interesting,” he says.

But the real benefit of formalisation in maths is now coming from the large corpus of existing formalised theorems, which allows human mathematicians to more readily build on top of them and also to train AI models that can help formalise new theorems faster. Training those AI models to formalise mathematics took time and lots of concrete examples to use as training data, which might not yet be available for physics.

“Ideally, we need a million lines of physics, and that might be hard work to get. If the machines aren’t pretty good at doing physics initially, then there’ll be manual work at the beginning, and then eventually the machines will hopefully take over,” says Buzzard.

The authors of the original physics paper didn’t respond to a request for comment but Tooby-Smith says that he informed them of his discovery, received confirmation that they agreed and was told that an erratum would be published.

First published on Fanatical Futurist on 26 March 2026.

311 Intelligence

What this means

Analysis by the 311 Strategic Intelligence Unit

The big shift is from trusting published results to checking them by machine. A formalisation language built for maths has found a fundamental error in a widely cited physics paper, and the researcher behind it fears many more papers harbour similar mistakes. We rate the Scientific Replication Crisis, failures to reproduce published results eroding trust in research, an Act now trend that already reached wide use in 2021. We track AI Formal Theorem Proving, AI that writes maths proofs a computer can check step by step, as an Explore technology with wide use by 2032.

What it means by sector.

• Universities and research funders: Tooby-Smith argues formalisation should become a standard part of publishing new research. That would add a new checking step before results are trusted.
• Publishers and journals: a single formalisation exercise exposed an error that years of citations missed. We rate Peer Review AI Overload an Act now trend, so machine checks could support strained reviewers.
• AI developers: Kevin Buzzard says physics would ideally need a million lines of formalised work to train AI models. Whoever builds that corpus will shape how quickly AI can check physics.

What to do now.

• If your products or decisions rest on published research, ask how key results have been checked, not just how often they are cited.
• Watch libraries such as PhysLib and MathsLib, which turn checked results into reusable building blocks.
• Fund or join efforts to formalise the research your field depends on, since that data is what trains future checking tools.

The Starburst technologies behind this story

From the 311 Technology Starburst (first product, expected wide use and readiness):

Technology	Category	First product	Wide use	Action	TRL
AI Formal Theorem Proving	Intelligence	2024	2032	Explore	6
Automated Mathematical Discovery Models	Intelligence	2025	2035	Explore	4
Step-Checking Reward Models	Intelligence	2025	2031	Explore	5
Neuro Symbolic Artificial Intelligence	Intelligence	2032	2034	Explore	6

And the trends they feed, from the 311 Trends Starburst:

Trend	Wide use	Action
Scientific Replication Crisis	2021	Act now
Peer Review AI Overload	2027	Act now
AI Accelerated Science	2030	Prepare

How this moves the trend

Machines have been moving steadily into the work of checking research. In 2023 ChatGPT was listed as an author on research papers, in 2024 we covered a new AI proof generator for software, and in 2025 Google and OpenAI AIs claimed gold at the International Maths Olympiad. Formal checking of physics is the next step.

Go deeper with 311

• The 311 Starburst Centre: every technology and trend above, with timelines and readiness.
• 311 Vantage: ask what machine-checked research means for your organisation and get a plain English executive brief.
• The Exponential Technology Codex and the Annual Trends Codex: the technologies and trends reshaping every industry.
• Book a briefing or keynote on the future of AI and science for your board or leadership team.