Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Joseph Tooby-Smith
hep-ph
Mar 9, 2026 · v1
TL;DR
Formalizes the two-Higgs-doublet-model potential stability in Lean with Physlib, uncovering an error in the 2006 literature.
Abstract
In 2006, using the best methods and techniques available at the time, Maniatis, von Manteuffel, Nachtmann and Nagel published a now widely cited paper on the stability of the two Higgs doublet model (2HDM) potential. Twenty years on, it is now easier to apply the process of formalization into an interactive theorem prover to this work thanks to projects like Mathlib and Physlib (the latter formerly PhysLean and Lean-QuantumInfo), and to ask for a higher standard of mathematical correctness. Doing so has revealed an error in the arguments of this 2006 paper, invalidating their main theorem on the stability of the 2HDM potential. This case is noteworthy because to the best of our knowledge it is the first non-trivial error in a physics paper found through formalization. It was one of the first papers where formalization was attempted, which raises the uncomfortable question of how many physics papers would not pass this higher level of scrutiny.
Problem
The 2006 paper by Maniatis, von Manteuffel, Nachtmann and Nagel on the stability of the two Higgs doublet model (2HDM) potential is widely cited in particle physics. The correctness of its main theorem had not been subjected to machine-checked verification.
Approach
The authors formalize the stability arguments of the 2006 paper into the Lean interactive theorem prover, using Mathlib and Physlib (formerly PhysLean). The formalization process applies a higher standard of mathematical correctness to the original arguments.
Results
Formalization revealed an error in the 2006 paper that invalidates its main theorem on the stability of the 2HDM potential. To the authors' knowledge, this is the first non-trivial error in a physics paper found through formalization, raising questions about how many physics papers would not survive this level of scrutiny.
