2769
Штучний інтелект починає змінювати сам спосіб, у який математики працюють із надзвичайно складними задачами. Якщо ще кілька років тому великі мовні моделі використовували переважно для пояснення вже відомих теорем або перевірки окремих кроків, тепер системи OpenAI, Anthropic, Google та інших лабораторій дедалі частіше допомагають знаходити нові зв’язки й підходи до проблем, які десятиліттями залишалися майже нерухомими.
Одним із головних сигналів цієї зміни стала серія недавніх результатів, де моделі не просто відтворювали відомі математичні аргументи, а пропонували нетривіальні напрямки дослідження. OpenAI повідомляла про значний прогрес на складних відкритих проблемах, Anthropic демонструвала результати у теоретичній математиці, а Google також активно розвиває системи, які працюють із формальними доказами та математичними міркуваннями.
Axios зазначає, що математична спільнота дедалі серйозніше ставиться до таких інструментів. Вони не замінюють ученого повністю, але можуть генерувати велику кількість гіпотез, перевіряти варіанти й шукати закономірності з такою швидкістю, яка недоступна окремій людині.
Показовим став підхід Anthropic до складних теоретичних задач. Дослідники дозволяли Claude тривалий час повертатися до однієї проблеми, перевіряти попередні спроби та будувати нові ланцюжки міркувань. У деяких випадках модель змогла покращити відомі теоретичні оцінки, не маючи наперед заданого готового шляху до результату.
Схожі експерименти проводять і в інших лабораторіях. Замість одного великого запиту системі можуть запускати сотні або тисячі агентів, які паралельно досліджують різні варіанти розв’язання. Потім результати порівнюють, відсіюють слабкі гіпотези та формалізують найперспективніші ідеї.
Важливу роль у цьому процесі відіграють формальні мови на кшталт Lean. Вони дозволяють математичному доказу бути перевіреним не лише людиною, а й спеціальною програмою, яка контролює кожен логічний крок. Це особливо важливо у випадку ШІ, оскільки мовна модель може формулювати переконливі, але неправильні твердження.
Комбінація генеративних моделей і формальної перевірки поступово змінює баланс між швидкістю пошуку і надійністю результату. Модель може запропонувати сотні напрямів, а автоматичний перевіряльник одразу відкидає ті, що містять логічні помилки.
Відомий математик Теренс Тао вважає, що дисципліна може перейти від традиційного дефіциту доказів до своєрідної «ери надлишку доказів». Якщо раніше головною проблемою було знайти хоча б один правильний шлях до складної теореми, у майбутньому дослідники можуть отримувати одразу десятки машинно перевірених варіантів і вже після цього обирати найбільш зрозумілі або концептуально цікаві.
Такий сценарій створює і нову проблему: математикам доведеться не лише доводити твердження, а й фільтрувати величезний потік машинно створених результатів. Не кожен формально правильний доказ є корисним для науки — важливо зрозуміти, чи пояснює він нову структуру, чи відкриває новий метод і чи можна на його основі побудувати подальші дослідження.
Попри це, останні результати показують, що ШІ переходить від ролі допоміжного калькулятора до активного учасника математичного пошуку. Саме ця зміна, на думку дослідників, може вплинути далеко за межами чистої математики — на фізику, медицину, інженерію, криптографію та теоретичну інформатику, де багато ключових задач напряму залежать від нових математичних методів.
https://www.axios.com/2026/09/08/ai-math-anthropic-openai-google
