كشف باحث يستخدم لغة 'لين' (Lean) للتحقق الصوري عن خلل جوهري في ورقة بحثية فيزيائية مؤثرة نُشرت عام 2006 حول نموذج 'هيجز' المزدوج (two Higgs doublet model). توصل جوزيف توبي-سميث من جامعة باث إلى هذا الاكتشاف أثناء بناء مكتبة لنظريات الفيزياء الموثقة. وقد أقر المؤلفون الأصليون بالخطأ ويعتزمون إصدار تصحيح له.
قام جوزيف توبي-سميث، الباحث في جامعة باث بالمملكة المتحدة، بتطبيق لغة البرمجة 'لين' (Lean) - المصممة للتحقق من البراهين الرياضية - على ورقة بحثية فيزيائية تعود لعام 2006 وتتناول استقرار جهد نموذج 'هيجز' المزدوج (2HDM). ادعت الورقة، التي حظيت باقتباسات واسعة منذ نشرها، أن شرطاً معيناً يُرمز له بـ C كافٍ لضمان حل مستقر. ومع ذلك، كشفت عملية التوثيق الصوري التي أجراها توبي-سميث عن مثال مضاد يفشل فيه الشرط C في تحقيق الاستقرار، مما يقوض النظرية في جوهرها. وصف توبي-سميث عمله بأنه خطوة روتينية لدمج النتيجة في PhysLib، وهي قاعدة بيانات متنامية للأبحاث الفيزيائية الموثقة على غرار مكتبة الرياضيات MathsLib. وقال: 'نحن لا نسعى لنقض الأوراق البحثية؛ بل نبني نتائج يمكن للجميع استخدامها'. وعلى الرغم من أن الخطأ يؤثر بشكل كبير على الورقة الأصلية، أشار توبي-سميث إلى أنه من غير المرجح أن يؤثر على الدراسات اللاحقة التي استشهدت بها. وقد أبلغ المؤلفين الذين أكدوا وجود المشكلة ويعتزمون نشر تصحيح. وتعد هذه هي المرة الأولى التي تحدد فيها مثل هذه البرمجيات خطأ في ورقة بحثية فيزيائية، مما يثير المخاوف بشأن وجود عيوب محتملة في أعمال أخرى. وأوضح توبي-سميث: 'بما أن الكثير من الفيزيائيين ليسوا مهتمين بهذه التفاصيل الدقيقة، فإنهم أحياناً يغفلون عنها، وهنا يقع الخطأ'. وأيد كيفن بوزارد من إمبريال كوليدج لندن توسيع نطاق التوثيق الصوري ليشمل الفيزياء النظرية، مسلطاً الضوء على فوائده في بناء مكتبات نظريات موثوقة وتدريب نماذج الذكاء الاصطناعي. وأشار إلى أن إنشاء مجموعة كبيرة من نتائج الفيزياء الموثقة سيتطلب جهداً بشرياً أولياً قبل أن تتمكن الآلات من المساعدة بفعالية أكبر. تظهر نتائج توبي-سميث في نسخة أولية على موقع arXiv (DOI: 10.48550/arXiv.2603.08139).