Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
This paper reports the discovery of a critical error in the 2006 Maniatis et al. analysis of the two Higgs doublet model potential's stability, which was identified through formalization in the Lean theorem prover and represents the first known non-trivial error in a physics paper uncovered by this rigorous method.