Наукові дослідження з фізики містять помилки: це вперше виявив комп'ютер

Комп'ютерна мова, створена для виявлення помилок у математичних теоремах, уперше виявила фундаментальну помилку в широко цитованій науковій статті з фізики. Вчений, який стоїть за цим відкриттям, каже, що це перша наукова стаття з фізики, яку він проаналізував у такий спосіб. Але дослідник побоюється, що багато наукових досліджень з фізики можуть містити помилки, пише Фокус.

У Фокус. Технології з'явився свійTelegram-канал. Підписуйтесь, щоб не пропускати найсвіжіші та найзахопливіші новини зі світу науки!

Спеціалізоване програмне забезпечення дедалі частіше використовують для того, щоб допомогти математикам перевірити правильність своїх теорій і виявити відсутність суперечностей і логічних помилок. Це робиться за допомогою процесу формалізації. Цей підхід навіть було запропоновано як потенційне вирішення деяких із найскладніших проблем у математиці.

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

Формалізовані теореми можна використовувати як будівельні блоки для формалізації складніших теорем.

"Ми не прагнемо спростовувати наукові дослідження, ми прагнемо отримати результати, які зможуть використати всі", — каже Тубі-Сміт.

Помилка пов'язана з твердженням, у якому автори наукової роботи з фізики стверджують, що певна умова C є достатньою для стабільного розв'язання задачі. Але Тубі-Сміт у процесі формалізації показав, що існує умова C, яка не забезпечує стабільного розв'язання.

Тубі-Сміт каже, що виявлення помилки сильно змінило наукове дослідження, але це навряд чи спричинить проблеми в наступних наукових роботах, які ґрунтуються на цій статті та цитують її.

Але тепер учений побоюється, що багато статей з фізики містять подібні помилки. Він вважає, що це переконливо доводить необхідність формалізації як стандартної частини публікації нових досліджень з фізики.

Тубі-Сміт каже, що фізики, як правило, не наводять стільки докладних відомостей у теоремах, скільки математики. Оскільки багато фізиків не зацікавлені в цих найдрібніших деталях, іноді вони їх упускають, і саме тут виникає помилка.

Вчений повідомив авторам дослідження про своє відкриття, отримав підтвердження їхньої згоди і йому сказали, що буде опубліковано виправлення.

Як уже писав Фокус, фізики вперше провели успішне транспортування антиматерії. Цей експеримент показав, що антиматерію можна доставити в спеціалізовані лабораторії, які допоможуть розгадати секрет античастинок.

Також Фокус писав про те, що китайці навчили роботів висловлювати емоції. Людиноподібні роботи можуть досягти успіху завдяки емоційній взаємодії з людьми, а не виконанню промислових завдань.

Під час написання матеріалу використано джерела: arXiv, New Scientist.