Lean Theorem Prover Catches First Non-Trivial Error in a Physics Paper, Exposing a Flaw in a Widely Cited Higgs Model Result
A University of Bath researcher used the Lean 4 theorem prover to formalize a 2006 particle physics paper and discovered its central stability theorem is false, marking the first time formal verification has uncovered a substantive error in published physics research.
Overview
A computer scientist at the University of Bath has demonstrated that formal verification tools developed for mathematics can catch real errors in published physics research. Joseph Tooby-Smith used the Lean 4 interactive theorem prover to formalize a widely cited 2006 paper on the stability of the two Higgs doublet model (2HDM) and found that its central theorem is demonstrably false, making this the first non-trivial error in a research-level physics paper identified through formal verification.
The discovery raises pointed questions about how many similar errors may be hiding in the broader physics literature, where mathematical arguments are often presented with less rigor than in pure mathematics.
What Happened
Tooby-Smith set out to formalize the results of a 2006 paper by Maniatis, von Manteuffel, Nachtmann, and Nagel, published in the European Physical Journal C, which presented conditions for the stability of the scalar potential in the general two Higgs doublet model. The 2HDM is a popular extension of the Standard Model of particle physics that adds a second Higgs doublet to the single one confirmed by the 2012 discovery of the Higgs boson at CERN.
The original paper claimed that a particular condition — referred to as condition C — was both necessary and sufficient for the stability of the 2HDM potential. During the formalization process, Tooby-Smith constructed an explicit counterexample: a potential that satisfies condition C but is nonetheless unstable. The counterexample was formally verified in Lean, leaving no room for ambiguity.
The task was originally intended as what Tooby-Smith described as a routine verification step to incorporate the result into PhysLib, the largest open-source library of formalized physics in Lean 4. PhysLib, which Tooby-Smith founded and maintains, currently has over 530 GitHub stars and more than 2,500 commits from a community of seven maintainers. It aims to become the physics equivalent of Mathlib, the established formal mathematics library for Lean, as outlined in his perspective paper in Advanced Science.
Tooby-Smith reported that he notified the original authors of his findings and received their acknowledgment, with confirmation that an erratum would be forthcoming, according to his preprint.
What It Means
The implications extend well beyond a single corrected theorem. In his perspective paper published in Advanced Science, Tooby-Smith has argued that interactive theorem provers are a class of programming language that can guarantee the correctness of mathematical definitions and theorems, and that physics stands to benefit from adopting them more widely.
The core challenge is that physicists generally provide less explicit detail in their theorems compared to mathematicians. Derivations in physics papers often rely on implicit assumptions, notational shortcuts, and physical intuition that are difficult to audit systematically. Formal verification forces every step to be made explicit, which is precisely how the error was caught — not through any sophisticated insight, but through the mechanical requirement that every logical step must be justified.
Tooby-Smith has noted in his preprint that this was his initial foray into systematically verifying published physics results, raising the uncomfortable question of how many physics papers would fail to survive this higher level of scrutiny.
What We Don’t Know
The practical impact of the specific error on downstream research remains unclear. Tooby-Smith has noted in the preprint that the flaw may not affect analyses that restrict themselves to quartic-only potentials, which is a common simplification in the literature. The extent to which other results that cite the original 2006 paper depend on the now-invalidated sufficiency claim has not been systematically assessed.
It is also unknown how representative this finding is. The 2006 paper was chosen for formalization not because it was suspected of containing errors, but as a standard reference in the field. Whether other widely cited results would survive the same treatment is an open question that PhysLib’s continued expansion may eventually help answer.
The Broader Landscape
The discovery arrives at a moment of growing interest in applying formal methods to the sciences. A team at the University of Maryland Baltimore County has used Lean to formalize results in chemical physics, including Langmuir and BET adsorption theories, and reported that the process revealed hidden assumptions missed in informal derivations, according to their paper published in Digital Discovery.
PhysLib itself covers high-energy physics and quantum information and has recently merged with the Lean-QuantumInfo library. The project operates under an Apache 2.0 license and emphasizes accessibility for physicists who may have no prior experience with formal methods, as described in Tooby-Smith’s Advanced Science paper.
The question Tooby-Smith’s work poses is not whether formal verification will become standard practice in physics — that remains a distant prospect given the field’s scale and the effort required to formalize even a single paper. The question is whether the errors it uncovers will be significant enough to change how physicists think about the reliability of their own literature.