形式検証言語「Lean」を用いた研究者が、2ヒッグスダブレットモデルに関する2006年の影響力のある物理学論文に根本的な誤りがあることを発見した。バース大学のジョセフ・トゥービー＝スミス氏は、検証済み物理定理ライブラリの構築中にこの発見に至った。原著者は誤りを認め、訂正論文を発表する予定である。
英国バース大学の研究者であるジョセフ・トゥービー＝スミス氏は、数学的証明を検証するために設計されたコンピュータ言語「Lean」を、2ヒッグスダブレットモデル（2HDM）ポテンシャルの安定性を検証した2006年の物理学論文に適用した。出版以来広く引用されてきた同論文では、Cと表記される特定の条件が安定した解を保証するために十分であると主張されていた。しかし、トゥービー＝スミス氏の形式化プロセスにより、条件Cが安定性をもたらさない反例が明らかになり、同論文の定理の核心が揺るがされる結果となった。トゥービー＝スミス氏は、この作業を数学ライブラリ「MathsLib」にならって構築中の形式化された物理学研究データベース「PhysLib」に結果を組み込むための日常的な手順であると説明した。「私たちは論文を反証するために取り組んでいるわけではありません。誰もが利用できる成果を積み上げるために取り組んでいるのです」と彼は述べた。この誤りは元の論文に大きな影響を与えるものの、これを引用したその後の研究には影響しない可能性が高いとトゥービー＝スミス氏は指摘している。彼が著者に通知したところ、著者は問題を認め、訂正論文を出版する意向を示した。物理学論文の誤りがこのようなソフトウェアによって特定されたのは今回が初めてであり、他の研究にも潜在的な欠陥があるのではないかという懸念を呼んでいる。「多くの物理学者はこうした細部に興味がないため、見落とすことがあり、そこに誤りが生じるのです」とトゥービー＝スミス氏は説明した。インペリアル・カレッジ・ロンドンのケビン・バザード氏は、信頼できる定理ライブラリの構築やAIモデルの学習に利点があるとして、理論物理学への形式化の拡大を支持した。同氏は、形式化された物理学の成果を十分に蓄積するには、機械がより効果的に支援できるようになるまで、初期段階での手作業による努力が必要になると指摘した。トゥービー＝スミス氏の研究結果は、arXivのプレプリントとして公開されている（DOI: 10.48550/arXiv.2603.08139）。
