Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Este artigo relata a descoberta, através da formalização em um provador de teoremas interativo, de um erro nos argumentos de um artigo amplamente citado de 2006 sobre a estabilidade do potencial do modelo de dois dupletos de Higgs, invalidando seu teorema principal e representando, até onde se sabe, o primeiro erro não trivial em um artigo de física identificado por meio dessa metodologia.