We have spent 20 years citing a theorem that a computer just proved is logically impossible.
Joseph Tooby-Smith, a researcher at the University of Bath, has just published a bombshell: using the Lean 4 formal verification tool, he found a non-trivial error in a foundational 2006 physics paper on the Two-Higgs-Doublet Model (2HDM). The original authors have agreed with the findings and will publish an erratum.
This marks the first documented case of formal verification tools — commonly used in mathematics and software — exposing a flaw in a published theoretical physics paper.
The Target: A 20-Year-Old Pillar of Particle Physics
The 2006 paper "Stability and Symmetry Breaking in the General Two-Higgs-Doublet Model" by Maniatis, von Manteuffel, Nachtmann, and Nagel has been cited hundreds of times. The 2HDM is one of the most important "Beyond the Standard Model" frameworks in particle physics — used to explain phenomena like Dark Matter and the matter-antimatter asymmetry of the universe.
In their Theorem 1, the original authors proposed a specific condition — Condition C — and claimed it was "necessary and sufficient" for the stability of the 2HDM Higgs potential. In plain language: they claimed this condition could definitively tell you whether the Higgs potential has a stable ground state (a "floor") or whether it collapses into an infinite energy sink.
The Discovery: Condition C Is Not Sufficient
While formalizing the mathematics of this paper into Lean 4 using the PhysLean library (the largest physics library in the interactive theorem prover Lean), Tooby-Smith found that Lean simply would not accept the proof of sufficiency.
This was not a software bug. It was the system doing exactly what it was designed to do: refusing to validate a logical step that is not logically valid.
- The Claim (2006): Condition C is necessary AND sufficient for stability
- The Reality (2026): Condition C is necessary, but NOT sufficient
- The Proof: Tooby-Smith constructed a formal counterexample — a specific version of the Higgs potential that satisfies Condition C but is mathematically unstable. This is formally verified in Lean: it is not an opinion, it is a mathematical certainty.
What Makes This Different From AI
This is not an "AI discovered something" story. Tooby-Smith explicitly stated there was "no extensive use of AI" (LLMs) in this work.
Unlike generative AI (ChatGPT, Gemini, Claude), which predicts likely outputs, Lean 4 is an Interactive Theorem Prover based on formal type theory. It doesn't guess. It doesn't hallucinate. Every single logical step must be mathematically perfect, or the system rejects it.
This is the same class of tools used to verify:
- Flight control software (Airbus uses formal methods)
- Microprocessor designs (Intel's division bug was found this way)
- The Four Color Theorem (formally verified in Coq/Lean)
Now, for the first time, this rigor has been applied to theoretical physics — and it found a bug.
The "Lindy Effect" Problem in Science
Science operates on a form of social proof: if a paper has been cited 500+ times over 20 years, the community assumes it must be correct. Peer review caught whatever errors existed. Hundreds of researchers built on its conclusions.
Except peer review is done by humans reading papers. Humans miss things. Formal verification does not.
As Tooby-Smith noted, this raises a profound question: If the first "easy" paper we formalized had a major error, how much of the rest of the physics literature is actually wrong?
PhysLean: Formalizing All of Physics
The PhysLean project (formerly HEPLean, now merged with Lean-QuantumInfo) is an open-source, community-run effort to formalize physics results into Lean. It is currently the largest physics library in any interactive theorem prover.
The vision: a future where every theorem in a physics paper can be checked by a computer before publication. Not replacing peer review — augmenting it with mathematical certainty.
The Bottom Line
For 20 years, the physics community built on a theorem that is provably wrong. A human with a logic engine found the error that thousands of human reviewers missed.
This is not the end of human physics. It is the beginning of formally verified physics — where "trust me, the math checks out" is replaced by "the computer verified every step."
The question is no longer whether formalization will come to physics. The question is: what else will it find?
Sources: arXiv: 2603.08139, New Scientist, PhysLean (GitHub), Bode Living