En forskare som använder formaliseringsspråket Lean har avslöjat en grundläggande brist i en inflytelserik fysikartikel från 2006 om "two Higgs doublet model". Joseph Tooby-Smith vid University of Bath gjorde upptäckten medan han byggde ett bibliotek med verifierade fysikteorem. De ursprungliga författarna har erkänt felet och planerar att publicera ett rättelseblad.
Joseph Tooby-Smith, forskare vid University of Bath i Storbritannien, använde datorspråket Lean – utformat för att verifiera matematiska bevis – på en fysikartikel från 2006 som undersöker stabiliteten i potentialen för "two Higgs doublet model" (2HDM). Artikeln, som varit flitigt citerad sedan publiceringen, hävdade att ett specifikt villkor, betecknat C, var tillräckligt för att säkerställa en stabil lösning. Tooby-Smiths formaliseringsprocess avslöjade dock ett motexempel där villkor C misslyckades med att ge stabilitet, vilket underminerar teoremets kärna. Tooby-Smith beskrev sitt arbete som ett rutinmässigt steg för att införliva resultatet i PhysLib, en växande databas med formaliserad fysikforskning modellerad efter matematikbiblioteket MathsLib. "Vi är inte ute efter att motbevisa artiklar; vi vill bygga resultat som alla kan använda", sade han. Även om felet påverkar den ursprungliga artikeln avsevärt, noterade Tooby-Smith att det är osannolikt att det påverkar efterföljande studier som citerat den. Han underrättade författarna, som bekräftade problemet och avser att publicera ett rättelseblad. Detta är första gången sådan programvara har identifierat ett fel i en fysikartikel, vilket väcker oro för potentiella brister i andra verk. "Eftersom många fysiker inte är intresserade av dessa detaljer missar de dem ibland, och det är där fel uppstår", förklarade Tooby-Smith. Kevin Buzzard vid Imperial College London förespråkade en utökning av formalisering till teoretisk fysik och betonade fördelarna för att bygga tillförlitliga teorembibliotek och träna AI-modeller. Han noterade att skapandet av en betydande mängd formaliserade fysikresultat kommer att kräva en initial manuell insats innan maskiner kan hjälpa till mer effektivt. Tooby-Smiths resultat finns i en förpublicering på arXiv (DOI: 10.48550/arXiv.2603.08139).
