Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
2026/03/09 by Joseph Tooby-Smith · 8 voices · 1 citation
#hep-ph #cs.LO #hep-th
paper · pdf
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.
Citations
Cited by
Discussions
- Non-trivial error in physics paper found via Lean [hn, 24 points, 2 comments]
- arxiv.org/abs/2603.08139 [bsky, 9 points, 0 comments]
- #arXiv Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature arxiv.org/abs/2603.08139 By using PhysLib, in a now widely cited paper on th [bsky, 6 points, 1 comments]
- Formalising a well-cited 20-year old physics paper on the stability of the two Higgs doublet model in Lean invalidates the main theorem! "It ... raises the uncomfortable question of how many physics p [bsky, 4 points, 0 comments]
- fork found in kitchen arxiv.org/abs/2603.08139 [bsky, 1 points, 0 comments]
- The error was found through the formalization process. This is the paper Tooby-Smith posted about the formalization: arxiv.org/pdf/2603.08139 [bsky, 1 points, 1 comments]
- Seems really cool. I don't have access to the article, but the paper referenced is this one arxiv.org/pdf/2603.08139 [bsky, 0 points, 0 comments]
- Formal theorem proving has long been a thing in some parts of the science world. Not the hand cranked version, but more automated. A widely cited particle physics paper from 2006 has just been found t [bsky, 0 points, 0 comments]
Related