Цифрова революція в математиці: чи зможе ІІ вирішити проблему доказів?
Протягом століть математика розвивалася приблизно так, як і сто років тому: люди записували ідеї на дошках, покладаючись на інтуїцію та текстові описи, щоб заповнити складні логічні прогалини. Однак зараз відбувається фундаментальне зрушення. Завдяки розвитку штучного інтелекту та руху у бік «формалізації», ця область прагне майбутнього, де математичні істини будуть не просто записані, а цифровим кодом закодовані та перевірені машинами.
Від інтуїції до коду: розквіт формалізації
В основі цієї трансформації лежить “формалізація” – процес перекладу математичних визначень і теорем у точний комп’ютерний код. На відміну від традиційних доказів, які можуть бути розтягнутими та спиратися на «поверхневі» описи, формалізований доказ має бути бездоганно суворим.
Не йдеться про те, що комп’ютер повинен «думати» за математика. Навпаки, сам математик має стати набагато дисциплінованішим, прописуючи кожен найменший логічний крок так, щоб спеціалізована програма могла перевірити його без найменшої двозначності.
Чому це важливо:
Сучасні математичні докази стають дедалі складнішими. У міру того, як дослідники об’єднують розрізнені галузі математики, докази можуть розтягуватися на сотні сторінок, що ускладнює їхній повний аналіз навіть для експертів-людей. Формалізація пропонує спосіб:
– Виключити людський фактор: Навіть одна галюцинація або логічна помилка може анулювати весь аргумент.
– Створити цифрову бібліотеку: Кодуючи математику, ми, по суті, будуємо «пошукову базу даних, що верифікується» всіх математичних знань.
– Звільнити людський інтелект: Якщо машини візьмуть на себе виснажливе завдання перевірки дрібних деталей, математики зможуть зосередитись на високому рівні творчості та нових відкриттях.
Орієнтир – «Велика теорема Ферма»
Щоб перевірити межі цієї нової парадигми, математик “Кевін Баззард” з Імперського коледжу Лондона взявся за одне з найскладніших завдань в історії: “Велику теорему Ферма”.
Хоча теорема була знаменито вирішена Ендрю Уайлсом в 1998 році, її доказ є потужним 130-сторінковим лабіринтом взаємопов’язаних математичних областей. Мета Баззарда – не «вирішити» її наново, а оцифрувати, використовуючи Lean – інтерактивний інструмент для доказу теорем.
Цей проект виявляється масштабним спільним підприємством. Те, що починалося як невелике дослідження, розрослося у міждисциплінарний феномен: тисячі повідомлень та десятки учасників працюють над тим, щоб перевести цей монументальний плід людської думки у формат, який машина читає.
Синергія ІІ: зустріч мовних моделей та доказників теорем
Найзначнішим каталізатором у цій галузі останнім часом стало злиття великих мовних моделей (LLM) — таких як ChatGPT — з доказниками теорем, такими як Lean.
Зараз LLM добре вміють імітувати стиль спілкування математиків, але вони ненадійні. Оскільки вони працюють на основі ймовірності, а не логіки, вони можуть видавати галюцинації, які виглядають правильними, але математично порожні. У математиці точність 99% рівносильна провалу.
Однак зараз зароджується новий гібридний підхід:
1. LLM пропонує потенційний доказ чи крок (тобто виконує «творчу» частину).
2. Доказник теорем (Lean) виступає в ролі остаточного фактчекер, перевіряючи кожну логічну ланку.
Ця синергія була нещодавно продемонстрована програмою ІІ Aristotle, яка використовувала Lean для досягнення результатів рівня золотої медалі Міжнародної математичної олімпіади.
Екзистенційне зрушення для науки
Цей технологічний стрибок не обходиться без суперечок. Математичне співтовариство зараз намагається відповісти на екзистенційне питання: * Чи не змінить прагнення цифрової точності саму природу математичних досліджень?
Існують обґрунтовані побоювання з приводу того, як ІІ може змінити роль математика і чи не загубиться «людський» елемент відкриття — інтуїція та боротьба — у морі автоматизованої перевірки. Проте прихильники процесу, такі як Патрік Шафто з Університету Ратгерса, припускають, що замість заміни людей ІІ підсвітить найцікавіші аспекти людської сутності: наше вроджене прагнення знань.
«Якщо ми оцифруємо математику, можливо, у якийсь момент це переверне математику з ніг на голову». – Кевін Баззард
Висновок
Перехід від паперу до коду є модернізацією математики, порівнянну з переходом від вінілу до стрімінгу музичної промисловості. Поєднуючи творчу міць ІІ з абсолютною суворістю цифрових доказників теорем, математика вступає в епоху, коли відкриття можуть бути прискорені, а істина може бути математично гарантована.
