Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
En formalisant la preuve de stabilité du potentiel du modèle à deux doublets de Higgs dans l'assistant de preuves Lean, les auteurs ont découvert une erreur invalidant le théorème principal d'un article de référence de 2006, marquant ainsi la première détection d'une telle erreur non triviale dans la littérature physique grâce à cette méthode.