У чому полягає відкриття?
Математична спільнота була приголомшена новиною про те, що агент штучного інтелекту зміг підтвердити правильність розв'язання надскладної задачі про упаковування сфер у багатовимірних просторах. Цей доказ, який стосується випадків у 8-вимірному та 24-вимірному просторах, приніс українській математикині Марині Вязовській престижну медаль Філдса у 2022 році. До її прориву ця задача була повністю розв'язана лише для одного, двох та трьох вимірів, тоді як усі інші варіанти залишалися відкритими протягом десятиліть, пише Live Science.
Дивіться також Google запускає Gemini у Chrome для нових країн і додає українську мову
Ця подія знаменує собою початок тихої революції. Протягом століть вчені використовували допоміжні засоби – від абака та логарифмічних лінійок до калькуляторів і комп'ютерів. Однак раніше ці інструменти лише прискорювали обчислення, не замінюючи людину в процесі міркування. Тепер ситуація змінилася: сучасні системи допомагають вибудовувати логічні ланцюжки й виконувати рутинні операції, що лежать в основі інтелектуальної праці.
Ключову роль у процесі верифікації відіграв ШІ-агент Gauss, розроблений стартапом Math. Він працював у тандемі з формальною мовою програмування Lean, яка спеціально створена для перевірки математичних аргументів. На відміну від звичайних наукових текстів, Lean вимагає абсолютної чіткості у кожному визначенні та висновку, виключаючи будь-які приховані припущення чи інтуїтивні стрибки. Якщо програма приймає аргумент, це гарантує його повну логічну коректність.
Процес верифікації виглядав як злагоджена робота команди: люди створили загальну структуру та концептуальний каркас доказу, а штучний інтелект заповнював прогалини. Ефективність машини виявилася дивовижною.
- Роботу над восьмивимірним випадком, яку дослідники планували виконувати протягом кількох місяців, алгоритм завершив лише за кілька днів.
- Складніша задача для 24-вимірного простору також була успішно вирішена невдовзі після цього.
Відомий математик Теренс Тао, який також є лауреатом медалі Філдса, зазначає, що головна цінність таких технологій полягає у звільненні науковців від рутинної роботи. Штучний інтелект бере на себе тисячі дрібних, хоча й логічно зрозумілих випадків, які забирають занадто багато часу при ручній обробці. Це дозволяє дослідникам зосередитися на стратегії та творчому пошуку ідей, залишаючи формальну перевірку машинам.
Водночас експерт Кевін Баззард з Імперського коледжу Лондона звертає увагу на важливу деталь: попри те, що великі мовні моделі можуть звучати переконливо, вони не гарантують точності. Саме тому використання спеціалізованих мов верифікації, таких як Lean, є критично важливим. Головним викликом залишається те, що більшість сучасної математики ще не перекладена на мову, зрозумілу таким системам.
Попри стрімкий розвиток технологій, учені переконані, що математики не зникнуть як професія. Навпаки, виникає гостра потреба у фахівцях, здатних ставити правильні питання, створювати нові концепції та розпізнавати справжню глибину ідей. Науковці майбутнього будуть дедалі більше нагадувати розробників складних інструментів, що поєднують людську інтуїцію з машинною наполегливістю для досягнення абсолютної впевненості у результатах.