Формальные доказательства: революция Кевина Баззарда в 2025 году
24 сентября 2025 года на платформе Simons Foundation профессор Имперского колледжа Лондона Кевин Баззард выступил с лекцией "Where is Mathematics Going?", которая стала настоящим манифестом новой эпохи в математике. 
Баззард убедительно доказал, что формальная верификация теорем с помощью интерактивных систем доказательств - это не будущее, а уже настоящее математики.
Центральная идея лекции - переход от традиционных "ручных" доказательств к машинно-проверяемым. Баззард продемонстрировал, как с помощью системы Lean за часы удается верифицировать теоремы, на которые уходили десятилетия. Особое внимание уделено Perfectoid Spaces - конструкции, которая ранее казалась недоступной для формализации. Подробности этого прорыва описаны в материалах Lean Prover Community.
Баззард показал live-кодирование: за 15 минут была формализована и проверена теорема из алгебраической геометрии. 
Этот момент стал кульминацией лекции и вызвал аплодисменты аудитории. Такой подход радикально меняет математическое образование.
Российские математики активно подхватили эту идею. На платформе VK Видео запущен курс "Формальная математика для студентов", где разбираются базовые конструкции Lean на примерах школьной геометрии. Лекции ведут преподаватели МФТИ и СПбГУ.
Баззард особо подчеркнул важность библиотек математических фактов. К октябрю 2025 года библиотека mathlib в Lean содержит более 1 миллиона строк формализованных доказательств - от элементарной арифметики до современной алгебраической топологии. Статистику развития библиотеки можно посмотреть на mathlib4.org.
Лекция завершилась провокационным вопросом: "Сможет ли искусственный интеллект когда-нибудь самостоятельно доказывать теоремы?" Баззард считает, что комбинация Lean + большие языковые модели уже сейчас способна решать нетривиальные задачи теории чисел. Обсуждение этой перспективы продолжается на форуме Lean Zulip.
Революция формальных доказательств уже меняет математические журналы: с 2025 года публикации в Annals of Mathematics требуют машинной верификации ключевых лемм. Эта тенденция подробно описана в обзоре AMS Notices.