Non-trivial error in physics paper found via Lean
10 hours ago
- #2HDM
- #Formal Verification
- #High Energy Physics
- A 2006 paper by Maniatis et al. on the stability of the two Higgs doublet model (2HDM) potential was widely cited.
- Formalization into an interactive theorem prover (using Mathlib and PhysLib) revealed an error in the 2006 paper, invalidating its main theorem.
- This is the first non-trivial error in a physics paper found through formalization.
- The discovery raises concerns about the validity of other physics papers under formal scrutiny.