Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
Este artículo documenta cómo la formalización en el asistente de pruebas interactivo Lean reveló un error en el teorema principal de un influyente artículo de 2006 sobre la estabilidad del potencial del modelo de dos dobletes de Higgs, marcando el primer hallazgo de un error no trivial en física mediante este método.