List view
**Authors:** Joseph Tooby-Smith We formalize the stability of the two Higgs doublet model into Lean. In doing so we show that there is an error in the widely cited paper [1]. This formalisation has been described in the paper [2]. Note that some PRs in this Milestone predate the review process now in place in Physlib. Also some bad pull-request management was done, meaning the some PRs have more than one logical change. **References** [1] M. Maniatis, A. von Manteuffel, O. Nachtmann, and F. Nagel. Stability and symmetry breaking in the general two-Higgs-doublet model. Eur. Phys. J. C, 48:805–823, 2006. arXiv:hep-ph/0605184, doi:10.1140/epjc/ s10052-006-0016-6. [2] J. Tooby-Smith. Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature. 2026. arXiv:2603.08139
No due date•6/6 issues closedBumping Physlib means moving it from one version of Lean to another. It often requires fixing theorems and definitions based on changes that have occurred in Mathlib.
No due date•28/28 issues closed