Un investigador que utiliza el lenguaje de formalización Lean ha descubierto un fallo fundamental en un influyente artículo de física de 2006 sobre el modelo de dos dobletes de Higgs. Joseph Tooby-Smith, de la Universidad de Bath, realizó el hallazgo mientras construía una biblioteca de teoremas físicos verificados. Los autores originales han reconocido el error y planean publicar una fe de erratas.
Joseph Tooby-Smith, investigador de la Universidad de Bath en el Reino Unido, aplicó el lenguaje informático Lean —diseñado para verificar pruebas matemáticas— a un artículo de física de 2006 que examinaba la estabilidad del potencial del modelo de dos dobletes de Higgs (2HDM, por sus siglas en inglés). El estudio, que ha sido ampliamente citado desde su publicación, afirmaba que una condición específica, denominada C, era suficiente para garantizar una solución estable. Sin embargo, el proceso de formalización de Tooby-Smith reveló un contraejemplo en el que la condición C no lograba producir estabilidad, lo que socava el teorema central. Tooby-Smith describió su labor como un paso rutinario para incorporar el resultado a PhysLib, una base de datos en crecimiento de investigación física formalizada, inspirada en la biblioteca matemática Mathlib. 'No estamos tratando de refutar artículos; estamos tratando de construir resultados que todos puedan utilizar', señaló. Aunque el error afecta significativamente al artículo original, Tooby-Smith observó que es poco probable que tenga impacto en estudios posteriores que lo citaron. Informó a los autores, quienes confirmaron el problema e intentarán publicar una fe de erratas. Esta es la primera vez que un software de este tipo identifica un error en un artículo de física, lo que suscita preocupación sobre posibles fallos en otros trabajos. 'Debido a que muchos físicos no están interesados en estos detalles minuciosos, a veces los pasan por alto, y ahí es donde se produce un error', explicó Tooby-Smith. Kevin Buzzard, del Imperial College London, respaldó la extensión de la formalización a la física teórica, destacando sus beneficios para crear bibliotecas de teoremas fiables y entrenar modelos de IA. Señaló que la creación de un cuerpo sustancial de resultados físicos formalizados requerirá un esfuerzo manual inicial antes de que las máquinas puedan ayudar de manera más efectiva. Los hallazgos de Tooby-Smith aparecen en una preimpresión en arXiv (DOI: 10.48550/arXiv.2603.08139).
