Recognition: no theorem link
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Pith reviewed 2026-05-15 14:21 UTC · model grok-4.3
The pith
Formalization of the two Higgs doublet model potential in Lean reveals an error that invalidates the main theorem of a 2006 paper.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
Encoding the mathematical statements of the 2006 paper into Lean shows that its proof of the stability theorem for the 2HDM potential contains an error, so the theorem no longer holds.
What carries the argument
The Lean formalization of the 2HDM potential and the bounded-from-below conditions that the 2006 paper claimed to characterize completely.
If this is right
- The stability criteria derived in the 2006 paper cannot be relied upon without correction.
- Any later work that adopts those criteria as complete must be re-examined for possible gaps.
- Formalization into Lean or similar systems can detect non-trivial errors in physics literature that earlier review processes missed.
- The first such error found this way raises the question of how many other published results would fail the same test.
Where Pith is reading between the lines
- Papers that cite the 2006 stability theorem as established fact may rest on shaky ground until the error is repaired.
- Routine use of interactive theorem provers could become a standard check for new calculations in model building.
- The same formalization approach could be applied to other long-standing results on scalar potentials in extensions of the Standard Model.
Load-bearing premise
The Lean code accurately captures the exact statements and steps of the 2006 paper without adding or omitting mathematical content.
What would settle it
An explicit counter-example potential that meets every condition listed in the 2006 theorem yet is unbounded from below, or a potential that the theorem deems unstable yet remains bounded.
read the original 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The manuscript describes the formalization of the stability conditions for the two-Higgs-doublet model (2HDM) scalar potential into the Lean interactive theorem prover, using libraries from Mathlib and Physlib. It claims that this process reveals an error in the arguments of the widely cited 2006 paper by Maniatis, von Manteuffel, Nachtmann and Nagel, invalidating their main theorem on the conditions for the potential to be bounded from below. The work positions itself as the first non-trivial physics error detected via formalization and raises broader questions about the rigor of pre-formalization literature.
Significance. If the Lean encoding is shown to faithfully reproduce the original 2006 statements without representational shifts, the result would be significant as a proof-of-concept for using theorem provers to audit complex stability analyses in beyond-Standard-Model physics. It highlights the value of machine-checked proofs for derivations involving quartic coupling matrices and bounded-from-below criteria, potentially setting a higher standard for future 2HDM and multi-Higgs studies.
major comments (1)
- The central claim that an error in Maniatis et al. (2006) invalidates their main stability theorem rests on the unverified assumption that the Lean definitions of the 2HDM potential V(Φ₁, Φ₂), the quartic coupling matrix, and the bounded-from-below criteria exactly match the 2006 statements. The manuscript provides no side-by-side comparison of the Lean code against the original equations, leaving open the possibility that any detected discrepancy is an artifact of the formalization rather than a genuine flaw in the source paper.
Simulated Author's Rebuttal
We thank the referee for their careful reading of the manuscript and for emphasizing the need to verify the fidelity of the formalization. We address the major comment below and will revise the manuscript accordingly to strengthen the presentation.
read point-by-point responses
-
Referee: The central claim that an error in Maniatis et al. (2006) invalidates their main stability theorem rests on the unverified assumption that the Lean definitions of the 2HDM potential V(Φ₁, Φ₂), the quartic coupling matrix, and the bounded-from-below criteria exactly match the 2006 statements. The manuscript provides no side-by-side comparison of the Lean code against the original equations, leaving open the possibility that any detected discrepancy is an artifact of the formalization rather than a genuine flaw in the source paper.
Authors: We agree that an explicit side-by-side comparison is necessary to fully substantiate the claim and rule out encoding artifacts. In the revised manuscript we will add a new section (or appendix) that reproduces the key equations from Maniatis et al. (2006) verbatim—specifically the scalar potential V(Φ₁, Φ₂), the definition of the quartic coupling matrix Λ, and the bounded-from-below criteria—directly alongside the corresponding Lean declarations and theorems. The Lean formalization was constructed by literal transcription of these expressions using the vector and matrix structures already present in Mathlib and Physlib; no representational shifts were introduced. The discrepancy we report concerns the logical structure of the 2006 proof (an incomplete case analysis in the stability argument), not the definitions themselves. Adding the requested comparison will make this distinction transparent. revision: yes
Circularity Check
No significant circularity; verification relies on external Lean/Mathlib benchmark
full rationale
The paper's derivation consists of encoding the 2006 Maniatis et al. statements into Lean using the independent Physlib/Mathlib libraries and then mechanically checking the original proof steps. This process is self-contained against an external theorem-prover benchmark whose semantics are not defined by the present manuscript. No equation or claim reduces by construction to a fitted parameter, self-citation chain, or renamed input; the detected discrepancy is reported as a direct consequence of the formalization rather than an internal redefinition. The faithfulness assumption is therefore an ordinary modeling choice, not a circular step.
Axiom & Free-Parameter Ledger
axioms (1)
- domain assumption The Lean formalization correctly and completely represents the mathematical statements and proof steps of the 2006 Maniatis et al. paper
Forward citations
Cited by 3 Pith papers
-
Formalizing CHSH Rigidity in Lean 4
The CHSH rigidity theorem is machine-checked in Lean 4, confirming near-optimal strategies are locally isometric to the qubit strategy while exposing a gap in prior reasoning.
-
Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization
Lean Atlas visualizes Lean 4 dependency graphs and applies Lean Compass to reduce the nodes needing human semantic review by 27-99% across six evaluated projects.
-
All LCA models are wrong. Are some of them useful? Towards open computational LCA in ICT
ICT LCAs form error-prone model systems requiring explicit dependency graphs and open versioned repositories for credible assessments.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.