Математическое доказательство представляет собой последовательность рассуждений, ведущих к определенному выводу. Lean, язык программирования, созданный в 2013 году Леонардо де Моурой из Рио-де-Жанейро, позволяет проверять эти доказательства для выявления ошибок или неточностей.
В сентябре Lean стал предметом споров после того, как OpenAI, компания-владелец ChatGPT, объявила о решении математической задачи Навье-Стокса, одной из Семи проблем тысячелетия, решение которых оценивается в 1 миллион долларов США каждое. Научное сообщество обсуждает, действительно ли эта демонстрация затрагивает первоначальный вопрос, хотя факт логической безупречности, который гарантирует Lean, является неоспоримым.
Эта возможность казалась немыслимой ни в 2023, ни в 2013 году. Автор рассказал, что работал в Microsoft, где теоремы проверяли сотрудники для обеспечения отсутствия ошибок в программном обеспечении. Однако этот метод был в десять раз дороже, чем внутренняя разработка программы, что ограничивало его использование критически важными секторами, такими как криптография. Никто не предвидел, что призеры премии Филдса, такие как Теренс Тао, начнут использовать эту систему. В настоящее время, когда кто-то обращается к Тао с заявлением о доказательстве гипотезы, его ответ таков: «Сначала проверьте в Lean».
Многие математики не знали о существовании Lean и задаются соответствующими вопросами, например, есть ли у него недостатки или можно ли ему доверять. В конкретном случае с Навье-Стоксом, содержащим сотни тысяч строк, написанных на Lean, члены сообщества изучили доказательство с помощью собственных созданных ими верификаторов, и оно было одобрено. Таким образом, кризис доверия больше связан с этическими вопросами, такими как заявления о чрезмерном потреблении воды или краже данных со стороны ИИ-компаний. Хотя это и актуальные темы, они не должны останавливать развитие математики.
Существуют различные реакции: одни проявляют энтузиазм, другие опасаются устареть, а третьи считают, что искусственный интеллект уничтожит математику. Питер Шолце, считающийся одним из величайших ныне живущих математиков, заявил, что умрет, не используя ИИ. С другой стороны, Кевин Баззард планировал пятилетний проект по формализации Великой теоремы Ферма в Lean. В апреле он посмеялся, когда ему спросили, поможет ли ИИ; через несколько месяцев ИИ выполнил работу всего за 11 дней. Автор заключает, что многие переживают «траур», сравнивая реакцию тех, кто выполнял вычисления в уме, с появлением калькулятора, который, несмотря на первоначальное сопротивление, принес пользу человечеству. Он научился не оспаривать ИИ.