Один из самых известных математиков мира, лауреат Филдсовской премии Терренс Тао стал гостем подкаста Лекса Фридмана. Что думает гениальный математик об искусственном интеллекте: 1️⃣ Текущее состояние: ИИ как помощник и «умный автокомплит» 🟡Lean как основа: Тао активно использует Lean для формализации доказательств. Сейчас это требует в 10 раз больше усилий, чем написание от руки, но позволяет организовывать массовые проекты с десятками участников (как его проект по проверке 22 миллионов алгебраических утверждений) и делает математику «бесконтактной» (trustless), где корректность проверяется машиной. 🟡Роль больших языковых моделей (LLM): В настоящее время ИИ выступает в роли «продвинутого автозаполнения» (fancy autocomplete). Он помогает находить нужные леммы в огромных библиотеках (Mathlib), предлагает варианты кода и ускоряет рутинные задачи. 🟡Недостатки: ИИ пока ненадежен. Он может «галлюцинировать» (придумывать несуществующие ссылки) или делать глупые ошибки, которые сложно заметить, потому что внешне сгенерированный текст или код выглядит безупречно. 2️⃣ Разрыв между человеком и ИИ: «Математическое чутье» 🟡Главное отличие: У человека-математика есть то, что Тао называет математическим чутьем» (a sense of smell) — интуитивное понимание того, какой путь доказательства является перспективным, а какой — тупиковым. У ИИ этого пока нет. 🟡Проблема «негативных данных»: ИИ обучается на опубликованных, успешных доказательствах. Он не имеет доступа к данным о тысячах неудачных попыток, ошибочных гипотезах и итеративном процессе поиска, который проходят люди. Тао шутит, что ИИ «нужно отправить в аспирантуру», чтобы он научился на ошибках. 🟡«Пасти кошек»: Попытка провести современный ИИ через известное доказательство, по словам Тао, похожа на «выпас кошек» (herding cats) — это требует больше усилий, чем доказать все самому. 3️⃣ Будущее математики: ИИ-коллега и «фазовый переход» 🟡«Фазовый переход»: Тао предсказывает момент (по аналогии с переходом на LaTeX), когда с помощью ИИ формализовать доказательство станет легче, чем писать его от руки. Это полностью изменит то, как математики работают и публикуют статьи. Журналы смогут принимать формализованные доказательства, что упростит проверку. 🟡ИИ как идеальный соавтор: В будущем ИИ станет партнером по диалогу. Математик сможет поручать ему проверку рутинных вычислений, поиск существующей литературы по теме, проверку гипотез для частных случаев («проверь для N до 100»), предложение новых идей и подходов. 4️⃣ Прогнозы 🟡ИИ как соавтор: Он предсказывал, что к 2026 году появятся совместные работы, и отмечает, что это уже происходит. 🟡ИИ, предлагающий гипотезу: Тао считает, что в течение этого десятилетия ИИ сможет предложить новую, значимую и, вероятно, верную гипотезу, связывающую разные области. 🟡ИИ, достойный Филдсовской премии: Это гораздо более отдаленная перспектива, но уровень сотрудничества будет углубляться.