Науковці виявили помилку в відомій фізичній статті, користуючись комп’ютерною мовою, розробленою для перевірки математичних теорій. Цей інструмент, який призначений для виявлення логічних помилок, вперше застосували для розкриття неточності в науковому дослідженні. Автор, Джозеф Тубі-Сміт з Університету Бата у Великій Британії, підкреслив, що це його перший досвід аналізу фізичної роботи таким чином, але висловив занепокоєння, що подібні помилки можуть зустрічатися й у багатьох інших наукових статтях.
Програмне забезпечення для формалізації дедалі частіше використовується в математиці для перевірки теорій на наявність суперечностей. Тубі-Сміт обрав документ, опублікований у 2006 році, який аналізував стабільність потенціалу моделі бозонів Гіггса. Під час формалізації він виявив, що одна з умов, яка вважалася достатньою для стабільного рішення, насправді не відповідає цій вимозі.
На думку Тубі-Сміта, виявлення цієї помилки свідчить про потребу впровадження формалізації у процес публікації наукових досліджень. Фізики часто не надають достатньо деталей у своїх теоріях, що може призводити до прогалин і помилок.
Науковець повідомив авторів роботи про своє відкриття, отримав підтвердження їхньої згоди на публікацію виправлення. Водночас Тубі-Сміт підкреслив, що багато інших статей з фізики можуть містити подібні недоліки.
Як приклад важливих досягнень у цій галузі, було нещодавно оголошено про успішне транспортування антиматерії, яке відкрило нові горизонти для досліджень античастинок. Також наголошувалося на проекті, метою якого було навчити роботів виражати емоції, що може зробити їхню взаємодію з людьми більш ефективною.
