Seorang peneliti yang menggunakan bahasa formalisasi Lean telah menemukan kelemahan mendasar dalam makalah fisika tahun 2006 yang berpengaruh mengenai model dua Higgs doublet. Joseph Tooby-Smith dari University of Bath membuat penemuan tersebut saat sedang membangun pustaka teorema fisika yang terverifikasi. Penulis asli makalah tersebut telah mengakui kesalahan tersebut dan berencana untuk menerbitkan erratum.
Joseph Tooby-Smith, seorang peneliti di University of Bath di Inggris, menerapkan bahasa komputer Lean—yang dirancang untuk memverifikasi pembuktian matematis—pada makalah fisika tahun 2006 yang mengkaji stabilitas potensial model dua Higgs doublet (2HDM). Makalah tersebut, yang telah banyak dikutip sejak diterbitkan, mengklaim bahwa kondisi tertentu, yang dilambangkan sebagai C, sudah cukup untuk memastikan solusi yang stabil. Namun, proses formalisasi yang dilakukan Tooby-Smith mengungkapkan contoh penyangkal di mana kondisi C gagal menghasilkan stabilitas, sehingga meruntuhkan teorema tersebut hingga ke intinya. Tooby-Smith menggambarkan usahanya sebagai langkah rutin untuk memasukkan hasil tersebut ke dalam PhysLib, sebuah basis data penelitian fisika formal yang sedang berkembang yang dimodelkan setelah pustaka matematika MathsLib. 'Kami tidak bertujuan untuk menyanggah makalah; kami bertujuan untuk membangun hasil yang dapat digunakan semua orang,' ujarnya. Meskipun kesalahan tersebut secara signifikan memengaruhi makalah aslinya, Tooby-Smith mencatat bahwa hal itu kemungkinan tidak berdampak pada studi selanjutnya yang mengutipnya. Ia telah memberi tahu para penulis, yang mengonfirmasi masalah tersebut dan berniat untuk menerbitkan erratum. Ini menandai pertama kalinya perangkat lunak semacam itu mengidentifikasi kesalahan dalam makalah fisika, yang memicu kekhawatiran tentang potensi cacat dalam karya-karya lain. 'Karena banyak fisikawan tidak tertarik pada detail-detail kecil ini, terkadang mereka melewatkannya, dan di situlah letak kesalahannya,' jelas Tooby-Smith. Kevin Buzzard di Imperial College London mendukung perluasan formalisasi ke fisika teoretis, menyoroti manfaatnya untuk membangun pustaka teorema yang andal dan melatih model AI. Ia mencatat bahwa menciptakan kumpulan hasil fisika formal yang substansial akan memerlukan upaya manual awal sebelum mesin dapat membantu dengan lebih efektif. Temuan Tooby-Smith muncul dalam pracetak di arXiv (DOI: 10.48550/arXiv.2603.08139).