Um pesquisador utilizando a linguagem de formalização Lean descobriu uma falha fundamental em um influente artigo de física de 2006 sobre o modelo de dois dubletos de Higgs. Joseph Tooby-Smith, da Universidade de Bath, fez a descoberta enquanto construía uma biblioteca de teoremas físicos verificados. Os autores originais reconheceram o erro e planejam publicar uma errata.
Joseph Tooby-Smith, pesquisador da Universidade de Bath, no Reino Unido, aplicou a linguagem computacional Lean — projetada para verificar provas matemáticas — a um artigo de física de 2006 que examinava a estabilidade do potencial do modelo de dois dubletos de Higgs (2HDM). O artigo, amplamente citado desde sua publicação, afirmava que uma condição específica, denominada C, era suficiente para garantir uma solução estável. No entanto, o processo de formalização de Tooby-Smith revelou um contraexemplo em que a condição C falhava em produzir estabilidade, comprometendo o teorema em sua base. Tooby-Smith descreveu seu trabalho como um passo rotineiro para incorporar o resultado à PhysLib, um banco de dados crescente de pesquisas físicas formalizadas, modelado a partir da biblioteca matemática Mathlib. 'Não estamos tentando refutar artigos; estamos tentando construir resultados que todos possam usar', afirmou. Embora o erro afete significativamente o artigo original, Tooby-Smith observou que é improvável que ele impacte estudos subsequentes que o citaram. Ele notificou os autores, que confirmaram a falha e pretendem publicar uma errata. Esta é a primeira vez que tal software identifica um erro em um artigo de física, levantando preocupações sobre possíveis falhas em outros trabalhos. 'Como muitos físicos não estão interessados nesses detalhes técnicos, às vezes eles deixam passar algo, e é aí que surge um erro', explicou Tooby-Smith. Kevin Buzzard, do Imperial College London, defendeu a extensão da formalização para a física teórica, destacando seus benefícios para a construção de bibliotecas de teoremas confiáveis e o treinamento de modelos de IA. Ele ressaltou que a criação de um corpo substancial de resultados físicos formalizados exigirá esforço manual inicial antes que as máquinas possam auxiliar de forma mais eficaz. As descobertas de Tooby-Smith aparecem em um preprint no arXiv (DOI: 10.48550/arXiv.2603.08139).