The Artificial Intelligence That Found a Hidden Flaw in Physics
Love it or hate it, Artificial Intelligence (AI) is proving its worth in weeding out errors in science. A case in point is the recent remarkable story whereby AI has exposed an error in a widely-accepted physics theorem.
A recent article in New Scientist has drawn attention to a quiet but potentially transformative moment in modern science: for the first time, a computer-assisted system has uncovered a significant error in a published physics paper. What might seem like a narrow technical correction instead opens a window onto a deeper shift in how scientific knowledge may be tested, verified, and trusted in the future.
The case centres on Joseph Tooby-Smith of the University of Bath, who was working with Lean, a specialised programming language designed to express mathematics in a form that a computer can rigorously check. His task was not especially dramatic: to formalise a 2006 study on the stability of the two-Higgs doublet model (2HDM), a theoretical extension of the Standard Model of particle physics. This effort formed part of a broader initiative to build a structured digital library of verified physics results.
Yet as the paper was translated into Lean’s unforgiving logical framework, something unexpected emerged. A condition long believed to guarantee stability did not, in fact, do so. What had appeared sound under conventional peer review contained a subtle but consequential gap—one that had gone unnoticed for years but became immediately visible when every logical step was forced into explicit form.
When informed, the original authors acknowledged the issue and indicated that a formal correction would follow. In this sense, the episode exemplifies the self-correcting nature of science. Errors are not failures so much as opportunities for refinement. However, the manner of discovery—through automated formal verification rather than human review—raises broader and more unsettling questions.
Why was the flaw missed in the first place? The answer lies partly in the differing cultures of physics and mathematics. In pure mathematics, proofs must be exhaustive and explicit, leaving no logical step unstated. In theoretical physics, by contrast, researchers often rely on intuition, approximation, and shared understanding. This approach has been extraordinarily productive, enabling rapid progress across complex domains. But it also leaves room for gaps—steps that are assumed rather than demonstrated, and which may escape even careful peer scrutiny.
Formal verification tools like Lean challenge this tradition. They require that every assumption be declared and every inference justified. There is no room for intuition or shorthand; the result is either logically valid or it is not. In exposing the flaw in the 2HDM paper, Lean did not “understand” the physics—it simply enforced consistency with absolute precision.
The implications extend well beyond a single corrected theorem. If similar methods were applied more broadly, they could serve as tireless auditors of scientific reasoning, identifying hidden inconsistencies before they propagate through the literature. Entire areas of theoretical work could be revisited, not out of suspicion, but out of a desire for deeper certainty.
Yet the transition to such a system is far from straightforward. Formalising even a single paper can require vast effort, translating dense theoretical arguments into thousands of lines of machine-readable code. Scaling this approach would demand the creation of an enormous digital infrastructure—a comprehensive library of formally verified physics. It would also require a cultural shift, as scientists adapt to new standards of rigor and new modes of communication.
There is, moreover, a delicate balance to maintain. Science thrives on creativity as well as precision. The risk of over-formalisation is that it could slow the exploratory, intuitive processes that often lead to breakthroughs. The challenge, then, is not to replace human insight, but to complement it—to pair imaginative theorising with uncompromising verification.
The episode highlighted by New Scientist ultimately reveals something fundamental about the nature of knowledge itself. Human reasoning, however sophisticated, is fallible, especially when confronted with extreme complexity. Machines, by contrast, offer a form of logical discipline that is both exacting and impartial. Together, they suggest a future in which scientific ideas are not only conceived by human minds but also tested against standards of rigor that no human alone could sustain.
If that future takes shape, discoveries like this may become increasingly common. What is remarkable today—a computer finding a hidden flaw in established theory—may soon become routine. And in that routine, science may find not only greater reliability, but a deeper understanding of its own foundations.
References
- New Scientist. (2026). For the first time, a computer found an error in a major physics paper.
- Joseph Tooby-Smith. (2026). Formalising the two-Higgs doublet model and identifying an error in a published stability proof. arXiv preprint (e.g., arXiv:2603.08139).
- Lean documentation and community resources (Lean Prover Project).
- University of Bath. Research context and affiliation of Joseph Tooby-Smith.
- Conway, N. (2026). Secondary summary of the New Scientist article (as cited in the original prompt).
About the author: John O’Sullivan is CEO and co-founder (with Dr Tim Ball among 45 scientists) of Principia Scientific International (PSI). He is a seasoned science writer, retired teacher and legal analyst who assisted skeptic climatologist Dr Ball in defeating UN climate expert, Michael ‘hockey stick’ Mann in the multi-million-dollar ‘science trial of the century‘. From 2010 O’Sullivan led the original ‘Slayers’ group of scientists who compiled the book ‘Slaying the Sky Dragon: Death of the Greenhouse Gas Theory’ debunking alarmist lies about carbon dioxide plus their follow-up climate book. His most recent publication, ‘Slaying the Virus and Vaccine Dragon’ broadens PSI’s critiques of mainstream medical group think and junk science.