A researcher using the Lean formalisation language has uncovered a fundamental flaw in a influential 2006 physics paper on the two Higgs doublet model. Joseph Tooby-Smith at the University of Bath made the discovery while building a library of verified physics theorems. The original authors have acknowledged the error and plan to issue an erratum.
Joseph Tooby-Smith, a researcher at the University of Bath in the UK, applied the Lean computer language—designed to verify mathematical proofs—to a 2006 physics paper examining the stability of the two Higgs doublet model (2HDM) potential. The paper, which has been widely cited since its publication, claimed that a specific condition, denoted as C, was sufficient to ensure a stable solution. However, Tooby-Smith's formalisation process revealed a counterexample where condition C failed to produce stability, undermining the theorem at its core. Tooby-Smith described his effort as a routine step to incorporate the result into PhysLib, a growing database of formalised physics research modeled after the mathematics library MathsLib. 'We’re not going out there to disprove papers; we’re going out there to build results that everyone can use,' he said. While the error significantly affects the original paper, Tooby-Smith noted it is unlikely to impact subsequent studies that cited it. He notified the authors, who confirmed the issue and intend to publish an erratum. This marks the first time such software has identified an error in a physics paper, prompting concerns about potential flaws in other works. '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,' Tooby-Smith explained. Kevin Buzzard at Imperial College London endorsed extending formalisation to theoretical physics, highlighting its benefits for building reliable theorem libraries and training AI models. He noted that creating a substantial body of formalised physics results will require initial manual effort before machines can assist more effectively. Tooby-Smith's findings appear in a preprint on arXiv (DOI: 10.48550/arXiv.2603.08139).