На протяжении веков математика развивалась примерно так же, как и сто лет назад: люди записывали идеи на досках, полагаясь на интуицию и текстовые описания, чтобы восполнить сложные логические пробелы. Однако сейчас происходит фундаментальный сдвиг. Благодаря развитию искусственного интеллекта и движению в сторону «формализации», эта область стремится к будущему, где математические истины будут не просто записаны, а цифровым кодом закодированы и проверены машинами.
От интуиции к коду: расцвет формализации
В основе этой трансформации лежит формализация — процесс перевода математических определений и теорем в точный компьютерный код. В отличие от традиционных доказательств, которые могут быть растянутыми и опираться на «поверхностные» описания, формализованное доказательство должно быть безупречно строгим.
Речь не о том, что компьютер должен «думать» за математика. Напротив, сам математик должен стать гораздо более дисциплинированным, прописывая каждый мельчайший логический шаг так, чтобы специализированная программа могла проверить его без малейшей двусмысленности.
Почему это важно:
Современные математические доказательства становятся всё более сложными. По мере того как исследователи объединяют разрозненные области математики, доказательства могут растягиваться на сотни страниц, что затрудняет их полный анализ даже для экспертов-людей. Формализация предлагает способ:
— Исключить человеческий фактор: Даже одна «галлюцинация» или логическая ошибка может аннулировать весь аргумент.
— Создать цифровую библиотеку: Кодируя математику, мы, по сути, строим «поисковую, верифицируемую базу данных» всех математических знаний.
— Освободить человеческий интеллект: Если машины возьмут на себя изнурительную задачу проверки мелких деталей, математики смогут сосредоточиться на высоком уровне творчества и новых открытиях.
Ориентир — «Великая теорема Ферма»
Чтобы проверить пределы этой новой парадигмы, математик Кевин Баззард из Имперского колледжа Лондона взялся за одну из самых сложных задач в истории: Великую теорему Ферма.
Хотя теорема была знаменито решена Эндрю Уайлсом в 1998 году, её доказательство представляет собой массивный 130-страничный лабиринт взаимосвязанных математических областей. Цель Баззарда — не «решить» её заново, а оцифровать, используя Lean — интерактивный инструмент для доказательства теорем.
Этот проект оказывается масштабным совместным предприятием. То, что начиналось как небольшое исследование, разрослось в междисциплинарный феномен: тысячи сообщений и десятки участников работают над тем, чтобы перевести этот монументальный плод человеческой мысли в формат, читаемый машиной.
Синергия ИИ: встреча языковых моделей и доказывателей теорем
Самым значительным катализатором в этой области в последнее время стало слияние больших языковых моделей (LLM) — таких как ChatGPT — с доказывателями теорем, такими как Lean.
На данный момент LLM отлично умеют имитировать стиль общения математиков, но они ненадежны. Поскольку они работают на основе вероятности, а не логики, они могут выдавать «галлюцинации», которые выглядят правильными, но математически пусты. В математике точность в 99% равносильна провалу.
Однако сейчас зарождается новый гибридный подход:
1. LLM предлагает потенциальное доказательство или шаг (т.е. выполняет «творческую» часть).
2. Доказыватель теорем (Lean) выступает в роли окончательного фактчекера, проверяя каждое логическое звено.
Эта синергия была недавно продемонстрирована программой ИИ Aristotle, которая использовала Lean для достижения результатов уровня золотой медали Международной математической олимпиады.
Экзистенциальный сдвиг для науки
Этот технологический скачок не обходится без споров. Математическое сообщество сейчас пытается ответить на экзистенциальный вопрос: не изменит ли стремление к цифровой точности саму природу математических исследований?
Существуют обоснованные опасения по поводу того, как ИИ может изменить роль математика и не потеряется ли «человеческий» элемент открытия — интуиция и борьба — в море автоматизированной проверки. Тем не менее, сторонники процесса, такие как Патрик Шафто из Университета Ратгерса, предполагают, что вместо замены людей ИИ подсветит самые интересные аспекты человеческой сущности: наше врожденное стремление к знаниям.
«Если мы оцифруем математику, возможно, в какой-то момент это перевернет математику с ног на голову». — Кевин Баззард
Заключение
Переход от бумаги к коду представляет собой модернизацию математики, сопоставимую с переходом от винила к стримингу в музыкальной индустрии. Объединяя творческую мощь ИИ с абсолютной строгостью цифровых доказывателей теорем, математика вступает в эпоху, когда открытия могут быть ускорены, а истина может быть математически гарантирована.
