Un chercheur utilisant le langage de formalisation Lean a découvert une faille fondamentale dans un article de physique influent de 2006 portant sur le modèle à deux doublets de Higgs. Joseph Tooby-Smith, de l'université de Bath, a fait cette découverte alors qu'il constituait une bibliothèque de théorèmes de physique vérifiés. Les auteurs originaux ont reconnu l'erreur et prévoient de publier un erratum.
Joseph Tooby-Smith, chercheur à l'université de Bath au Royaume-Uni, a appliqué le langage informatique Lean – conçu pour vérifier des preuves mathématiques – à un article de physique de 2006 étudiant la stabilité du potentiel du modèle à deux doublets de Higgs (2HDM). L'article, largement cité depuis sa publication, affirmait qu'une condition spécifique, désignée par C, suffisait à garantir une solution stable. Cependant, le processus de formalisation de Tooby-Smith a révélé un contre-exemple où la condition C ne permettait pas d'assurer cette stabilité, remettant ainsi en cause le cœur du théorème. Tooby-Smith a décrit son travail comme une étape de routine visant à intégrer le résultat dans PhysLib, une base de données croissante de recherches en physique formalisées, inspirée de la bibliothèque mathématique MathsLib. 'Nous ne cherchons pas à réfuter des articles ; nous cherchons à établir des résultats que tout le monde peut utiliser', a-t-il déclaré. Bien que l'erreur affecte considérablement l'article original, Tooby-Smith a noté qu'il est peu probable qu'elle impacte les études ultérieures qui l'ont cité. Il a informé les auteurs, qui ont confirmé le problème et prévoient de publier un erratum. Il s'agit de la première fois qu'un tel logiciel identifie une erreur dans un article de physique, ce qui soulève des inquiétudes quant aux failles potentielles dans d'autres travaux. 'Comme beaucoup de physiciens ne s'intéressent pas à ces détails techniques, il leur arrive de passer à côté, et c'est là que survient l'erreur', a expliqué Tooby-Smith. Kevin Buzzard, de l'Imperial College London, a soutenu l'extension de la formalisation à la physique théorique, soulignant ses avantages pour la création de bibliothèques de théorèmes fiables et l'entraînement de modèles d'IA. Il a noté que la création d'un corpus substantiel de résultats de physique formalisés nécessitera un effort manuel initial avant que les machines ne puissent aider plus efficacement. Les conclusions de Tooby-Smith figurent dans une prépublication sur arXiv (DOI : 10.48550/arXiv.2603.08139).