Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Dit artikel beschrijft hoe formalisatie in Lean een fout heeft blootgelegd in een veel geciteerde 2006-publicatie over de stabiliteit van het twee-Higgs-dubbelletmodel, wat het eerste geval is van een niet-triviale fout in de natuurkunde die via deze methode is ontdekt.