Hacker News Digest

Появление больших языковых моделей уже приносит реальные математические результаты: построение решения с конечным временем обострения для уравнений Навье–Стокса с вынуждающим членом и предложенное доказательство квази-гипотезы Римана заслуживают самого пристального внимания математиков. Однако их значимость требует постоянной независимой проверки и осмысления сообществом. Особенно хорошо модели работают с доказательствами на языке Lean, но для по-настоящему трудных теорем такие формальные доказательства достигают сотен тысяч строк кода. Тревожная тенденция: чем длиннее Lean-доказательство, тем более запутанным и менее точным оказывается его машинный перевод на естественный язык — и никто не понимает почему. В итоге для важнейших задач мы получаем корректные формальные доказательства, которые невозможно прочесть напрямую, и хаотичные пересказы, требующие огромных усилий для человеческого понимания. Возникает фундаментальный вопрос: без человеческого понимания зачем вообще заниматься математикой и получать доказательства, кроме как для тестирования моделей?

Автор рассматривает два сценария. «Золотой век» — осторожная интеграция моделей в научную экосистему с приоритетом поддержки нового поколения учёных, развития экспертизы и сохранения открытой, коллаборативной и интеллектуально независимой науки. «Тёмный век» — впечатляющий рост научной продукции в краткосрочной перспективе при прогрессирующем ослаблении самостоятельной человеческой научной деятельности: производство знаний сосредоточится в немногих руках, а сами эти руки будут всё хуже понимать созданное. Настоящая тьма — знание, ставшее чуждым человеческому пониманию.

Реальность, вероятно, соединит оба сценария. Конкретные шаги к «золотому веку»: доступ исследователей к передовым моделям, стандарты воспроизводимости и раскрытия для созданной с их помощью науки, ресурсы на осмысление и распространение таких результатов, изучение влияния моделей на научное образование и подготовку кадров, а также устойчивые инвестиции в публично управляемую инфраструктуру. Математикам автор отводит особую ответственность — сохранить математику живой частью человеческой культуры, принимая неопределённость, используя все инструменты для открытия нового и создавая лучшие профессиональные стандарты для следующих поколений.

Главная проблема ИИ в математике — не отсутствие ответов, а отсутствие процесса обучения человека через объяснение и интуицию. Спор: ИИ умеет решать, но не обучать (@ttul, @curt15) vs. если результат достигнут, человеческое понимание становится вторичным (@0c3ca83, @charcircuit). Риск: научные открытия могут превратиться в закрытые проприетарные патенты корпораций (OpenAI, Anthropic), создавая новые «дзайбацу» и ограничивая доступ к знаниям (@jacquesm). Опыт @rustyhancock: «вайб-кодинг» с ИИ лишает разработчика глубокого изучения паттернов и ошибок, degradируя навыки обучения в работе. Спор: ИИ — заслуженный удар по интеллектуальному снобизму и гейткипингу (@augment_me, @hbcdbff) vs. утрата культурного наследия. Будущее науки зависит от выбора между моделью жесткой конкуренции (ведущей к «темным векам» и закрытости) и моделью сотрудничества (@itsalwaysgood, @joe_the_user). ИИ может демократизировать математику, убрав барьеры сложной нотации и иерархической системы именования теорем в честь авторов (@grandpajoey).

Фонд Саймонса совместно с Anthropic и OpenAI вкладывает 15 миллионов долларов, чтобы помочь математикам адаптироваться к стремительному распространению искусственного интеллекта. Фонд будет управлять средствами и распределять их, в том числе через открытый конкурс заявок, поддерживая семинары и инициативы: оценку результатов, полученных с помощью ИИ, освоение новых инструментов, обмен мнениями и выработку общих стандартов использования ИИ. Anthropic и OpenAI также предоставят исследователям свои ИИ-инструменты и вычислительные ресурсы — причём не только в математике, но и в фундаментальной науке.

Президент фонда Дэвид Спергел подчёркивает: «Сейчас время взглянуть на математику как на целое — не как на набор доказательств и теорем, а как на коллективное понимание, движимое человеческим любопытством». По его словам, именно сообщество, а не отдельная компания или институт, должно определять, как эти инструменты оценивают, принимают и используют. Фонд давно поддерживает машинное обучение для науки: он финансировал разработку ассистента доказательств Lean, который изменил работу математиков и сделал возможными доказательства с помощью ИИ, а также проводил семинары и лекции о роли ИИ в этой области.

Обсуждение носит преимущественно скептический характер: пользователи воспринимают инициативу как PR-ход компаний OpenAI и Anthropic, выражают опасения по поводу несправедливого распределения грантов и деградации навыков математиков.

• Спор: Спор о распределении средств: @muragekibicho считает, что деньги получат уже известные и обеспеченные ученые (например, Terrence Tao), в то время как @schrototo утверждает, что гранты в академии обычно идут на найм PhD-студентов и постдоков.

• Спор: Мнения о целях компаний: @mrandish и @efficient_dairy видят в этом «отбеливание» репутации и способ получить бесплатную обратную связь от экспертов для улучшения моделей, тогда как @dannyw считает, что у фонда нет скрытой повестки, так как он давно поддерживает arXiv и науку.

• Совет: По опыту @an0malous, ученым следует отключать опции «Improve model for everyone» в настройках ChatGPT и Claude, чтобы избежать скрапинга их работ после публикации.

• Спор: Риски для когнитивных навыков: @lhk931122 на примере собственного опыта в разработке отмечает, что использование ИИ ухудшает навыки кодинга, и опасается, что математики перестанут понимать структуру доказательств, созданных ИИ.

• Сумма в 15 миллионов долларов воспринимается многими (@chazeon, @cuttothechase, @allears) как незначительная («карманные деньги») для таких гигантов, как OpenAI и Anthropic, и недостаточная для реальных системных изменений.

• Спор: Философский спор о сути математики: @tarkin2 задается вопросом, не пропадет ли ценность процесса поиска решения и интеллектуального роста, если ИИ будет выдавать только конечный результат.

OAI and Ant got blowback for essentially strip mining mathematical discoveries into PR wins for their models, accidentally laying waste to the research field in process. Throwing ~$5M each into PR whitewashing (partially in token credits), seems self-serving. — @mrandish

Перевод: OpenAI и Anthropic подверглись критике за то, что фактически «вырабатывали» математические открытия ради PR-побед своих моделей, попутно разрушая исследовательскую среду. Вброс по ~5 млн долларов на PR-отбеливание (частично в виде токенов) выглядит как попытка удовлетворить собственные интересы.

Математика переживает переход от эпохи дефицита доказательств к эпохе их изобилия благодаря развитию ИИ. Традиционно поиск и проверка доказательств требовали глубокой экспертизы и были редки, что формировало институты и стимулы математической науки. Однако доказательства обладают уникальными свойствами: они объективно проверяемы, легко оцифровываются и могут быть верифицированы машинами, например, в системах типа Lean. Это делает математику идеальной мишенью для современных ИИ-моделей, которые уже способны решать многие открытые задачи за короткое время без специального prompting от пользователя. Однако способности ИИ крайне неровны: впечатляющи в формальных, данных-rich задачах, но слабы там, где требуется субъективная оценка или взаимодействие с реальным миром.

Несмотря на прогресс, большинство проблем на переднем крае математики остаются нерешёнными — пространство задач бесконечно, а их сложность неограниченна. Поэтому будущее математики — «Math 2.0» — должно выходить за рамки простого поиска доказательств. Нужно смещать фокус с количества на качество: использовать ИИ для выявления новых принципов, методов и инсайтов, улучшать существующие доказательства, исследовать «окрестности теорем», строить интерпретируемые и безопасные открытые математические модели. Примеры включают Maththon — студенческий марафон по улучшению доказательств, IEANTN — динамическую сеть результатов в аналитической теории чисел, и ablation studies — проверку устойчивости théorems при удалении посылок. Главное препятствие для Math 2.0 — не технологии или культура, а воображение: умение видеть, как ИИ может углубить понимание, а не просто автоматизировать поиск.

Кризис в математике — не технологический, а культурный: утрата смысловых стимулов, идентичности и институциональных механизмов признания. Математики теряют традиционные пути к признанию — решение открытых задач, коллаборации, приглашения на конференции — из-за того, что AI-лишает их этих возможностей. AI-доказательства часто не интегрируются в математическую «кодовую базу», поскольку строятся с нуля, без опоры на существующие теории, что делает их бесполезными для дальнейшего развития. Спор: одни считают, что понимание механизма AI не требуется для его применения (как в медицине), другие — что понимание остаётся фундаментальной целью чистой математики, и его отказ разрушает её суть. Сравнение с программированием: математики сталкиваются с доказательствами, которые не могут интерпретировать, как разработчики с непонятным кодом — это эволюция профессиональной реальности. Современная наука (медицина, инженерия) уже работает с полуэмпирическими моделями (SPICE, анестезия), и это не мешает использованию. Критика Тао за пример с раком — проекция страха; его аргументы о стерильности поля и разрушении путей признания остаются релевантными. Математика как культура переживает трансформацию: ценности, стимулы и иерархии изменятся, но сама математика выйдет сильнее. AI не заменяет понимание, а меняет его природу: люди могут переключиться с решения на анализ, интерпретацию и улучшение AI-доказательств — удовольствие от математики в понимании, а не в решении. Опасение: AI может генерировать «бесполезные» доказательства (экспоненциально сложные, без инсайтов), отвлекая от глубоких закономерностей. Эпистемологическая проблема: если AI «бегает» по доказательству, но человек не видит этапов, как доверять результату? Это не решается только формальной верификацией. AI уже меняет практику: исследователи переписывают гранты, бросают годы работы, чувствуют себя ненужными — реальное поведенческое смещение. Тао не против AI — он предупреждает, что человечество может перестать развивать «путь к свету», а будет только добираться до «светильников» без понимания их работы. Сравнение с программированием: «vibe proving» AI может привести к хаотичному, неподдерживаемому математическому «коду», как «vibe coding» разрушает качество ПО. Наука всегда адаптировалась к новым инструментам (калькуляторы, компьютеры); кризис — это переход, а не конец, но адаптация требует осознанности. Совет: математикам следует переключиться с решения задач на анализ, рефакторинг и объяснение AI-доказательств — это новая форма творчества, сохраняющая человеческую роль.

Dan Roberts объявил об обновлении GitHub-репозитория с математическими формализациями в Lean: добавлено шесть новых формализаций, внесено 19 правок и отозвано три ранее опубликованные рукописи. На данный момент около 42% ключевых результатов из исходного набора формализовано в системе доказательств Lean. Команда планирует продолжать пополнять репозиторий новыми формализациями и исправлять обнаруженные неточности. Отозванные работы касаются алгебраичности классов Вейля на расщепленных абелевых восьмеричных многообразиях, соответствия Кuga–Satake для поверхностей K3 и рациональной гипотезы Ходжа для произведений поверхностей K3. Обновление подчеркивает растущую роль формальной верификации в математике, где доказательства обрабатываются как программный код, подверженный релизам, правкам и откатам. Репозиторий доступен по ссылке в твите.

Обсуждение подчеркивает, что без активного участия математического сообщества ошибки в AI‐сгенерированных доказательствах остаются незамеченными, даже если они прошли формальную проверку в Lean. Низкий уровень ошибок (3 из ~400) воспринимается как тревожный, и предлагается разделять проверенные и потенциально ошибочные результаты, привлекая профессиональных математиков для контроля качества. Большинство согласны: автоматическая проверка в Lean не заменяет человеческую экспертизу — без сообщества ошибки, такие как знаковая, останутся незамеченными, и доверие к результатам пострадает. Есть разногласия: @hmate9 считает три отказа из ~400 приемлемым уровнем для экспериментального проекта, тогда как @ijustlovemath и @ThePhysicist настаивают, что любые ошибки недопустимы, так как подрывают доверие к AI‐доказательствам. Рекомендуется публиковать результаты в двух частях: проверенные в Lean и требующие дополнительной проверки, чтобы избежать путаницы. Некоторые советуют OpenAI финансировать лабораторию ведущих математиков, работающих с моделью, для надёжной проверки и репутации проекта. Особое внимание вызывают «слишком хорошие» результаты, например, доказательство ускорения умножения целых чисел ниже O(n log n), которые могут скрывать ошибки и требуют тщательной верификации.

OpenAI выпустила 372 математических результата, среди которых доказательство Уникальной игры-гипотезы (UGC) — центральной проблемы в теории приближённых алгоритмов, над которой работала жена автора, теоретик сложности Дана Мошковиц. Хотя доказательство сопровождается сертификатом в системе Lean, оно настолько запутанно и плохо написано, что пока не понятно ни одному человеку без помощи ИИ. Дана описывает текст как «написанный кем-то на психоделиках», полный бессвязных ссылок и рекурсивных конструкций, напоминающих «чужеродный код», и отмечает, что даже базовые утверждения о полноте и корректности приходится вытягивать из разных частей работы с помощью ИИ-ассистента Astra. Однако она также отмечает важный побочный результат: авторы получили прямое доказательство NP-трудности аппроксимации для Max CSP и других задач, обходя UGC, что само по себе является прорывом. Несмотря на шок от того, что машина решила проблему всей её карьеры, Дана чувствует и облегчение — гипотеза оказалась верной, как она всегда верила. Автор подчеркивает, что теперь всё математическое сообщество оказалось в одной лодке: предстоит долгая работа по осмыслению и проверке этих доказательств, что может открыть новую эру сотрудничества человека и ИИ в математике, где творческие идеи человека будут проверяться и реализовываться машиной. Помимо UGC, среди результатов есть доказательства L = BPL и другие, которые также требуют тщательного анализа. Сообщество должно оценить, насколько соблюдены принципы ответственного выпуска таких систем, и решить, какие дальнейшие шаги нужны для equitable доступа к этим инструментам.

Тред добавляет практические цифры о стоимости решения открытых задач, критикует качество и проверяемость AI‐доказательств, подчёркивает необходимость человеческой проверки и адаптации подходов к выбору задач, а также обсуждает возможные ошибки в Lean и перспективы доступа математики к моделям. По данным @ZeljkoS, модель решает ~5 % от 8 000 тестовых задач, что эквивалентно 60 часам вычислений и примерно $810 за одно доказательство при текущих ценах GPT‐Pro. Многие участники отмечают, что доказательства не проверены: Lean‐код может быть сформулирован неверно, а сам текст слишком запутан, чтобы понять без ИИ. AI‐генерируемые доказательства описываются как «мусорный» код, требующий тщательной проверки, что делает работу благодарственной, но малоценной. Совет: Математики должны пересмотреть выбор задач, ориентируясь на те, которые модель может решить за ограниченное время, чтобы эффективно использовать AI. Использовать AI для объяснения, проверки и написания более понятных доказательств, а не только для их генерации. Обеспечить доступ математики к моделям, чтобы они могли участвовать в процессе, а не только наблюдать. Спор: Некоторые считают доказательства достоверными, другие сомневаются из‐за неясного изложения и возможных ошибок в Lean. @olalonde и @d--b поднимают вопрос о том, что AI мог найти и использовать баг в Lean, что ставит под сомнение надёжность проверок. @TMWNN цитирует DCKP, что PhD‐студенты могут решать задачи с публичными моделями за 15 минут, но остаётся вопрос эффективности в ограниченное время. Совет: PhD‐студенты, обеспокоенные утратой навыков, должны искать новые роли, где AI служит инструментом, а не заменой.

Автоматическое формализование текста из естественного языка в системы вроде Lean не гарантирует корректности исходного доказательства, даже если формальная версия проходит проверку. Проблема заключается в том, что семантически верный перевод математических утверждений из естественного языка в формальный язык требует разрешения неоднозначностей, которые формально невычислимы и находятся на самом высоком уровне иерархии вычислимой сложности (SCI = ∞), что делает задачу строго сложнее, чем проблема останова. Это означает, что никакой алгоритм, включая ИИ, не может гарантировать faithful перевод во всех случаях. На практике это приводит к ситуациям, когда формальное доказательство в Lean подтверждает что-то отличное от того, что утверждалось в естественном языке. В качестве примера авторы анализируют заявленное доказательство взрыва решений уравнений Навье–Стокса, сгенерированное ИИ и формализованное в Lean: хотя Lean-проверка проходит, формализованное утверждение не соответствует исходному естественноязычному claim, то есть доказано не то, что заявлено. Таким образом, доверие к результатам ИИ-доказательств на основе их формальной верификации вводит в заблуждение, поскольку разрыв между естественным и формальным языком остаётся фундаментальным и не преодолимым автоматическими средствами.

Формальное доказательство в Lean считается корректным, но не гарантирует соответствие оригинальному естественноязыковому доказательству. Участники подчеркивают необходимость независимой проверки и отмечают типичные проблемы неоднозначности при переводе математики в формальный язык. Это не опровергает заявленную «доказанность» Navier‐Stokes, а ставит под вопрос эквивалентность двух формулировок. Большинство согласны, что Lean‐доказательство проверяется ядром Lean, но может доказывать формулировку, отличную от той, что в статье. Проблема несоответствия естественноязыкового и формального доказательства типична: спецификация часто отличается от кода, как в человеческих проектах. Ключевой вопрос — эквивалентность формализованного утверждения Lean с оригинальной формулировкой задачи Клейского института. Если они эквивалентны, несоответствие текста не влияет на валидность результата. Естественноязыковые математические утверждения содержат неоднозначности, которые невычислимы и требуют экспертного вмешательства при формализации. Некоторые сравнивают ситуацию с случаями, когда формальная проверка выявляла ошибки в оригинальном тексте (например, статья о borrow‐checker). Есть разногласия: один набор участников считает, что несоответствие показывает лишь различие в формулировках; другой указывает, что это может вводить в заблуждение относительно того, что именно доказано, и требует уточнения, какие утверждения действительно доказаны. Рекомендуется рассматривать AI‐сгенерированные доказательства как «утверждения», требующие традиционного рецензирования и независимой проверки перед принятием как окончательные результаты. Автоматические проверяющие не противоречат теоремам Гёделя, поскольку они лишь проверяют уже найденные доказательства, а не генерируют их для произвольных утверждений.

OpenAI выпустила результаты, полученные внутренней frontier-моделью в математике, включая формализацию доказательств в Lean и детали о вычислениях. Результаты опубликованы в GitHub-репозитории с протоколами для правок и цитирования, разработанными при консультациях с Advisory Group on Mathematics and Artificial Intelligence при Institute for Advanced Study. Для прозрачности добавлены 10 суммариев рассуждений модели, статистика по решённым задачам и оценка вычислений: средний результат потребовал эквивалент трёх часов работы ChatGPT Pro. OpenAI планирует улучшать качество публикаций через лучшую экспозицию и цитирование, а также финансировать workshops и конференции по理解 AI-генерированных математических результатов. Компания продолжит оценивать свои модели на научных задачах и действовать на основе обратной связи от сообщества, стремясь ответственно делиться передовыми возможностями для ускорения прогресса в науке.

Обсуждение подтверждает, что OpenAI достигла беспрецедентного прогресса в формализованной математике, решив десятки открытых проблем, включая Unique Games Conjecture и Barnette's Conjecture, что вызывает у математиков эмоциональную и профессиональную дислокацию, а также ставит под сомнение будущее академической исследовательской работы.

• Unique Games Conjecture теперь считается доказанной, что переписывает основы теории приближённых алгоритмов и делает алгоритмы вроде Goemans-Williamson оптимальными в пределах полиномиального времени.

• Barnette's Conjecture, над которой пользователь @jboggan работал 24 года, был решён, что вызывает у него и других исследователей чувство утраты, несмотря на признание значимости результата.

• Средний результат требовал эквивалент трёх часов вычислений ChatGPT Pro, что демонстрирует невероятную эффективность и масштабируемость подхода OpenAI.

• Решены четыре из семи задач тысячелетия: Hodge, Birch-Swinnerton-Dyer, Riemann и Navier-Stokes, при этом P vs NP и Yang-Mills остаются нерешёнными, что указывает на ограничения текущих методов.

• Доказательства, опубликованные OpenAI, отличаются читаемостью и структурой, в отличие от генерируемого ChatGPT, что говорит о специфической настройке модели для математической формализации.

• Согласно @qnleigh, многие результаты подтверждают давно предполагаемые физические гипотезы, но формализуют их строго, что имеет значение для математической физики, но не всегда для физиков.

• Решена задача трёхмашинного планирования unit-job, открытая с 1979 года, что демонстрирует способность модели решать давние проблемы в теории расписаний.

• Каталанова константа доказана иррациональной — результат, признанный значимым, хотя и не относящийся к задачам тысячелетия, но важный для теории чисел.

• OpenAI решила 90 из 500 наиболее значимых открытых проблем математики, включая Hilbert’s tenth problem over Q, Hadwiger и Nonexistence of Landau–Siegel zeros.

• Математики, такие как @Turneyboy, сообщают, что их собственные многолетние проекты были полностью обесценены одним релизом, что вызывает глубокую депрессию в академическом сообществе.

• Автономный математический агент @kbr- уже решил 12-летнюю открытую проблему в proof complexity, что подтверждает, что подобные достижения не уникальны для OpenAI.

• Решение задачи умножения целых чисел ниже n log n (задача 109) и невозможность раскраски плоскости пятью цветами (задача 158) показывают неожиданные прорывы в фундаментальных областях.

• Публикация на GitHub, а не в платных журналах, воспринимается как революционный шаг к открытой науке, особенно в контексте критики @karahime о gatekeeping в академии.

• Совет: Пользователь @open592 задаёт вопрос о будущем PhD-студентов, чьи работы были обесценены — это указывает на необходимость пересмотра структуры академического обучения и защиты диссертаций.

• Спор: @nuclearsugar ссылается на статью Quanta, где исследователи соревновались с ИИ в доказательстве Unique Games, тогда как @nuclearsugar и другие считают, что ИИ опередил их, а не сотрудничал — это вызывает спор о природе сотрудничества между человеком и ИИ.

As Kevin Buzzard recently said:> In a 2020 piece in the Notices of the AMS, I asked the following question: “If one human had an understanding of all of modern pure mathematics simultaneously, how much further would they immediately be able to see?” Six years later we are beginning to understand… — @xanderlewis

Перевод: Как недавно сказал Кевин Баззард: «В статье 2020 года в Notices of the AMS я задал вопрос: „Если бы один человек обладал полным пониманием всей современной чистой математики, насколько дальше он смог бы заглянуть?“ Шесть лет спустя мы начинаем понимать ответ на этот вопрос.

Автор, будучи новичком в математике, попытался доказать гипотезу Конвея о свойстве уточнения omnific целых чисел с помощью больших языковых моделей и ассистента Lean. Он потратил месяц свободного времени и около 40 миллиардов токенов (с оценкой стоимости в $40 000), получив машинно проверенное доказательство в Lean, которое прошло проверку в реестре Palomar и получило предварительное одобрение от специалистов, знакомых с Lean и теорией сюрреалистических чисел. Хотя независимой верификации математиками нет, автор считает доказательство корректным и приглашает к опровержению. Он подчеркивает, что чисто ИИ‑подход возможен, но требует значительной инженерной работы и управления агентами, и считает, что наибольшую ценность такие инструменты принесут сами математикам, если будут использоваться в гармонии с их исследованиями.

Использование LLM для создания машинно-проверенных математических доказательств — новая спорная практика. Ценность здесь заключается не в авторстве, а в способности человека направлять и валидировать работу ИИ без глубокой экспертной подготовки. Дискуссии вокруг этого метода разделили участников на два лагеря. Одни считают такой подход «эксплуатацией человеческого капитала» и «stripmining» академических знаний, утверждая, что автор не заслуживает признания, если лишь оплачивал токены и задавал вопросы, не понимая сути. Другие полагают, что умение управлять LLM, формулировать запросы и интегрировать результаты в строгие формальные системы — это редкий навык, требующий интеллекта. Сдвиг в вычислительной культуре характеризуется переходом от «волшебников», понимающих систему, к «колдунам», использующим непонятные силы. Это подчеркивает различие между «know-that» (знания от LLM) и «know-how» (глубокое понимание). При этом доступность изложения новичка часто делает сложную математику понятнее традиционных лекций. Ключевым вкладом является использование Lean и Palomar для машинной проверки, что обеспечивает надежность и задает новый стандарт, где такая проверка становится обязательной. Процесс постоянной перепроверки результатов напоминает работу опытных разработчиков, а не пассивное потребление. Рекомендации по работе с LLM в математике: * не принимать результаты без объяснений, проверять логику и требовать ответственности за каждое утверждение; * упрощать доказательства, искать паттерны, сопоставлять части с известными теоремами; * использовать LLM в роли критика из научного журнала для углубления понимания; * проверить литературу на предмет дублирования доказательства. Ограничения и проблемы: * Экономическая неустойчивость: затраты в $40 000 за 40 миллиардов токенов зависят от личных ресурсов, а не от системной поддержки. * Интеллектуальный барьер: LLM пока не способны формулировать глубокие нетривиальные гипотезы на уровне Конвея; один из комментаторов назвал ИИ «великим фильтром», застрявшим на локальном максимуме развития. * Проблема признания: чтобы вклад был воспринят серьезно, автору следует демонстрировать глубокое понимание контекста, а не просто исправлять опечатки в письмах математикам.

Bend — это быстрый язык программирования с синтаксисом, похожим на Python, который компилируется в нативный код и достигает скорости C на одном ядре, а на 16 ядрах или GPU — до 100x ускорения. Его ключевая особенность — встроенная система доказательств, вдохновлённая Lean и Rocq, которая позволяет формально проверять свойства кода. Типовый проверятель Bend работает за секунду, что делает его пригодным для использования ИИ-агентами после каждого изменения.

Благодаря LAWS.bend разработчики могут объявлять неизменяемые правила (например, «победа невозможно»), которые ИИ не может нарушить — любая попытка нарушить закон блокируется на этапе проверки. Пример с игрой показывает, что без LAWS.bend ИИ допускает ошибку (слияние клеток), а с ней — вынужден исправлять код, пока не докажет корректность. Bend автоматически параллелизует код без потоков или блокировок, распределяя вычисления по доступным ядрам или GPU-ядрам. Для начала работы достаточно установить Bend через скрипт и добавить рекомендации в AGENTS.md: запускать bend guide, соблюдать LAWS.bend, проверять PROOF.bend перед коммитом и параллелизовать всё возможное. Язык ориентирован на бэкенд, Linux и macOS, и позиционируется как инструмент для создания надёжных, высокопроизводительных систем в эпоху ИИ-генерируемого кода.

Скептицизм вызывает удалённая история коммитов, отсутствие changelog и сомнения в реальной производительности Bend на GPU, особенно из-за обещанного 100‐кратного ускорения при непараллелизуемых доказательствах. Также отмечаются ограничения системы доказательств, необходимость чёткой документации и сравнения с CUDA, Futhark, Ada/SPARK, Dafny и Lean. Большинство считают язык интересным экспериментом, но пока без практических кейсов и бенчмарков. Рекомендуется восстановить историю коммитов, добавить changelog, заморозить базовые аксиомы и предоставить библиотеку законов, чтобы избежать их подгонки под новые функции. Текущий планировщик критикуется за плохую балансировку нагрузки (например, в n‐queens). Bend подходит для балансированных рекурсивных вычислений над ADT, но не для плотных массивных задач. Вопрос о поддержке M‐Series GPU остаётся открытым — заявлена только CUDA, а цифры для macOS вызывают сомнения. Автор признаёт, что год работы без отдыха ограничил примеры и документацию. Нужны более детальные примеры, бенчмарки и сравнение с Lean, Agda и другими системами. Формальные доказательства требуют высокого когнитивного усилия, что может быть барьером. Пользователи отмечают, что базовые законы (например, коммутативность сложения) часто приходится писать заново. Есть опасения, что плохие законы могут привести к неожиданным ошибкам («monkey paw»‐сценарий).

Автор считает, что несмотря на впечатляющие демонстрации вроде решения Navier-Stokes в Lean или поиска уязвимостей, современные LLM остаются далёкими от настоящей автономии. Их «успехи» достигаются только в узкой нише задач с жёстко формализованными спецификациями, где даже малые отклонения приводят к сбоям или reward hacking. Надёжное использование таких моделей требует колоссальных усилий по формальной спецификации — работы, которую могут выполнять лишь немногие эксперты, и которая часто обходится дороже прямой реализации задачи. Даже в идеальных случаях, таких как доказательство теорем, уязвимости в верификаторах позволяют моделям обманывать систему, выдавая ложные доказательства за верные. Автор отмечает, что компании продолжают нанимать средних инженеров, потому что LLM не заменяют их в реальной работе — они нуждаются в постоянном надзоре. Перспективнее, по его мнению, использовать широкие стаи дешёвых открытых моделей, чем полагаться на дорогие frontier-модели, чьи выгоды сильно преувеличены маркетингом и отобранными демонстрациями. Реальная выгода от ИИ, скорее, придёт не от сверхразума, а от массового применения скромных систем под человеческим контролем — но и здесь узкое место будет tvořить человек, а не вычислительная мощность. Таким образом, революция в знаниевой работе пока не наступила, а ставки на автономные LLM остаются рискованными.

Тред дополняет тезис о неспособности современных LLM к автономии. Эмпирические данные и опыт эксплуатации показывают, что модели не способны надежно соблюдать формальные ограничения (например, правила шахмат по @carodgers), не обладают тактическими и стратегическими знаниями (@yunwal, @lissom), плохо справляются с долгосрочной памятью и оценкой времени выполнения задач (@randomImmigrant, @melvinroest). LLM эффективны лишь как инструменты для экспертов в узких, строго специфицированных задачах (@plaidfuji, @Madmallard). Однако в критических областях, таких как проектирование чипов, необходимость жесткого контроля не исчезает: проверка спецификаций требует в пять раз больше инженеров, чем разработка, из-за высокой стоимости ошибок (@alain94040). Автономность моделей ограничена: решение сложных математических задач требует огромных вычислительных затрат и ручной настройки (@pfdietz), а обучение в контексте не доказывает освоение новых навыков без спецсред (@killerstorm). Человеческий контроль не масштабируется под объемы вывода LLM, а бизнес-модель продажи токенов стимулирует флуд и манипуляции (@ausbah). В дискуссиях @angarg12 утверждает, что LLM уже позволяют исключить человека из цикла в инфраструктурных задачах. @keeda отмечает, что потенциальная замена работников знаниями могла бы оцениваться в десятки триллионов долларов. Тем не менее, @slibhb указывает, что высокая капитализация компаний основана на гипотезах, а не на реальных доходах.

OpenAI объявил о доказательстве, решившем давнюю задачу по уравнениям Навье-Стокса, но ключевой момент, упущенный в обсуждениях, — это одновременная публикация формального доказательства в системе Lean 4 alongside человекочитаемой версии. Это отражает растущую тенденцию: многие недавние математические доказательства, поддержанные ИИ, теперь сопровождаются машинно-проверяемыми формализованными версиями, особенно в Lean 4. До недавнего времени создание таких доказательств было крайне трудоёмким процессом — по оценкам 2005 года, формализация одной страницы учебника по математике требовала около сорока часов работы, что делало её непрактичной для плотных научных статей, где одна фраза может ссылаться на десятилетия предшествующих исследований. Однако прогресс в инструментах и ИИ-ассистентах начал снижать этот барьер, делая формальную верификацию всё более осуществимой даже для сложных результатов. Это изменение может трансформировать математическую практику, повышая надёжность и прозрачность доказательств в эпоху ИИ.

Помимо формального доказательства, обсуждаются огромные вычислительные затраты (до $40 млн на агентный кластер, $132 млн против человеческого труда), сомнения в оригинальности (возможное копирование шагов из чужих работ), медленная верификация Lean-кода (15 часов против 11 дней генерации), риски багов в системе и необходимость проверки, что код действительно формализует заявленную теорему. Традиционная формализация 166-страничного текста требует 132 800 человеко-часов. Несмотря на важность автоформализации, её применение требует глубокого опыта в Lean и математической базе. Рекомендуется оптимизировать верификатор, использовать параллельные вычисления и развивать компактные модели, работающие на потребительском железе. Вопрос о возможности человеческой верификации AI-доказательств остаётся открытым — одни сомневаются в понимании, другие полагаются на формальные системы.

OpenAI объявила о решении задачи Навье–Стокса о существовании и гладкости, одной из семи проблем тысячелетия. Внутренняя система компании доказала, что уравнения Навье–Стокса для трёхмерной несжимаемой жидкости с постоянной плотностью могут развить сингулярность за конечное время, даже если начальное движение гладкое. Сингулярность здесь означает неограниченный рост скорости жидкости, несмотря на наличие вязкости, которая обычно подавляет такие эффекты. Результат опубликован в виде научной работы и формализован в системе проверки теорем Lean, что позволяет независимо проверить корректность доказательства.

Проблема оставалась открытой около 90 лет и имеет ключевое значение для гидродинамики, инженерии и климатического моделирования. OpenAI подчеркивает, что доказательство получено с использованием внутренней модели, значительно превосходящей GPT‑6 Astra, и стремится продемонстрировать темпы прогресса ИИ в решении фундаментальных научных задач. Компания призывает к ответственному использованию таких технологий и видит в этом шаге вклад в развитие исследований, полезных для всего человечества.

OpenAI продемонстрировала резкий скачок в математических способностях ИИ: менее чем за две недели система превзошла Astra, решив задачу, нерешённую 26 лет, с использованием 4,9 млн сообщений и 300 млрд токенов за 5 дней — ресурсы, недоступные академическим исследователям. Использование Lean для формализации доказательства с первого дня повысило доверие к результатам, но вызвало этические споры. Критики утверждают, что OpenAI, возможно, использовала промпты и предварительные результаты других исследователей, включая работы Тристана Бакмасстера и Левента Альпёге, а также слухи о нерешённой задаче для ускоренного запуска проекта — что ставит под сомнение оригинальность, нарушает традиции открытой науки и создаёт опасный прецедент: корпорация тратит $15 млн, чтобы «перехватить» результат, достигнутый годами работы академика. OpenAI утверждает, что не использовала данные других исследователей, но не исключает, что модели обучались на деидентифицированных пользовательских промптах, что вызывает подозрения в научном плагиате и неэтичной конкуренции. Утверждения о «строгих мерах безопасности» воспринимаются как попытка смягчить обвинения. Математики выражают тревогу: годы обучения становятся менее ценными, карьерные возможности сужаются, а авторство открытий перераспределяется в пользу корпораций. ИИ пока эффективен в поиске контрпримеров и сингулярностей, но не в построении глубоких теорий — его роль ограничена опровержением, а не созданием нового знания. Это смещает приоритеты математики в сторону опровержения гипотез. Советы: открытые модели предпочтительнее закрытых, чтобы избежать присвоения чужих идей; следующим вызовом для ИИ должно стать формализование классификации конечных простых групп — чтобы проверить его способность не только решать, но и систематизировать математику.

Математик и его коллега Левант Альпоге объявили о достижении конечного времени взрыва с гладким принуждением для трёх систем: уравнения несжимаемой пористой среды, системы Буссинеска и трёхмерных уравнений Эйлера. Они считают, что также получили взрыв для гипо-диссипативных уравнений Навье-Стокса, но не публикуют этот результат, поскольку проверка в Lean ещё не завершена, а рукопись не готова к публикации. Работа построена на программе Диего Кордобы и Луиса Мартинеса-Зороа, которые несколько лет исследовали вынужденные взрывы с грубым принуждением; авторы использовали большие языковые модели (LLM), чтобы довести эту программу до гладкого принуждения и уравнений Эйлера. Идеи лежат в основе работ Кордобы и Мартинеса-Зороа, и автор считает, что Мартинес-Зороа заслуживает медали Филдса за этот вклад.

Сотрудничество с Левантом было личным, без институциональной поддержки. Использовались модели Anthropic’s Claude, OpenAI’s Codex (включая GPT-5.6 Sol) и recientemente Astra — последняя только для написания и аудита аргументов. Прогресс был медленным до середины августа, когда 15-го числа получены результаты для Буссинеска и Эйлера с гладким принуждением; первая LLM-доказательная версия, полученная от Леванта, была ужасна, но проверена в Lean 22-го числа. С тех пор авторы работают круглосуточно, чтобы превратить машинное доказательство в читаемое. Автор извиняется за низкое качество написания статей, называя их «AI slop», и объясняет это внешним давлением и спешкой. Он подчеркивает, что настоящая значимость результата — не в самом взрыве, а в том, что математик и LLM смогли достичь этого за месяц, что ставит под вопрос традиционные модели обучения, авторства и рецензирования в математике, сравнивая этот момент с «Deep Blue — Каспаровым».

Автор также раскрывает конфликт: после объявления результатов ему предложили через Себастьяна (представителя OpenAI) удалить Леванта из авторства под предлогом, что OpenAI якобы собирается опубликовать собственный результат по Навье-Стоксу и заявить, что они заслуживают Клейевской премии, а авторы — «ближайшие люди к проблеме». Автор отказался, заявив, что если OpenAI опубликует своё решение таким образом, он сделает публичным то, что ему сказали. Он подчеркивает, что не видел доказательства OpenAI, не обвиняет никого, но считает необходимым рассказать о предложении, чтобы предотвратить ложную narraтиву. В завершение он благодарит математическое сообщество за поддержку и выражает желание вернуться к обсуждению идей Кордобы и Мартинеса-Зороа и broader implications для математики.

Тред обсуждает спор о возможном использовании OpenAI приватных данных исследователей Buckmaster–Alpöge при работе над доказательством для уравнений Навье–Стокса: прямых доказательств копирования нет, но существует значительное недоверие. Утверждается, что OpenAI могла получить доступ к их сессиям Codex — компания это отрицает. Также упоминаются якобы имевшие место угрозы со стороны сотрудников OpenAI против соавтора, связанного с Anthropic — они отвергаются как ложные. Неясно, началась ли работа OpenAI над задачей до или после известия о прогрессе Buckmaster–Alpöge, что вызывает споры о мотивации ускорения. При этом подтверждено, что Buckmaster и Alpöge активно использовали Claude и Codex в процессе разработки. Многие считают, что инцидент приведёт к ужесточению ограничений на использование публичных LLM для конфиденциальных исследований. Рекомендуется избегать ввода черновиков доказательств в публичные интерфейсы до ясности условий использования. Предлагается разработать общепринятые нормы атрибуции и лицензирования при значительном вкладе LLM в математические доказательства.

Клод, ИИ-модель от Anthropic, за 11 дней автономно создал первое полностью компьютерно проверенное доказательство Великой теоремы Ферма в системе доказательств Lean. Он написал 13 миллионов строк кода и доказал 29 500 промежуточных теорем, охватив алгебру, гармонический анализ, геометрию и теорию чисел. Это достижение подтверждает, что теорема верна исключительно на основе аксиом математики, без дополнительных предположений. Кевин Бззард отметил, что доказательство многослойное и достаточно надёжное, чтобы служить основой для дальнейших исследований. Автоматическая формализация таких сложных доказательств открывает путь к будущему, где любые математические результаты можно будет быстро и надёжно верифицировать, снижая нагрузку на сообщество при оценке новых работ. Это особенно важно, учитывая историю ошибок в математике — от сотен ложных попыток доказать FLT до летних споров вокруг доказательств гипотез Пуанкаре и Голдбаха. Теперь ИИ может помочь сделать математику более прозрачной и доверенной.

Формализация Великой теоремы Ферма в Lean знаменует сдвиг в методологии математики, требуя пересмотра доверия к проверке, масштабу и воспроизводимости доказательств. Контекст проекта можно уточнить в блоге Кевина Баззарда (Imperial College), а исторический фон — в книге Саймона Сингха. Доказательство охватывает только случай p≥17; для меньших простых теорема уже доказана. Объём кода (~13 млн строк) вызывает сомнения в полной безошибочности: ядро Lean ранее уже имело эксплуатируемые уязвимости, что создаёт риск скрытых ошибок. Некоторые считают такой код «чёрным ящиком» — нечитаемым в отличие от человеческих доказательств. Стоимость формализации составила ~$300k по тарифам API, что делает проекты экономически осуществимыми, но не массовыми. Платформа Prove2Me показала, что человеческие инструменты критически важны и при автономной работе ИИ. Часть кода предлагается внести в Mathlib, чтобы сохранить вклад для сообщества. Для будущих формализаций рекомендуют Metamath с его минимальным ядром проверки. Для масштабных проектов потребуются системы управления задачами (например, JIRA), а для изучения Lean — качественный учебник, так как текущие ресурсы недостаточны. Достижение показывает, что ИИ способен формализовать сложнейшие теоремы (включая потенциальную классификацию конечных простых групп) и синтезировать конструкции за пределами существующих библиотек. Это снижает нагрузку на рецензентов, однако формализация не опровергает оригинальное доказательство Уайлса, а лишь подтверждает его строгой логикой, не заменяя человеческого понимания.

OpenAI представил десять прорывных результатов в математике и теоретической информатике, полученных с помощью внутренней версии модели Astra. Среди них — новые верхние оценки плотности упаковки сфер в высоких размерностях, достигнутые вплоть до порога Коэна–Элкиса, и экспоненциально улучшенные границы для максимального размера двоичных кодов при заданном минимальном расстоянии. Также решены задачи в теории кодирования, сложности арифметических схем, квантовой сложности и решёточной криптографии. Все доказательства были формализованы в системе Lean и сопровождаются пошаговыми объяснениями модели.

Общая стоимость вычислений для нахождения решений составила около $2000 по тарифам Sol API. Каждое решение сопровождается аудио-навигацией мышления модели и человеческой редактурой. Это первый масштабный пример, когда ИИ не просто помогает, а самостоятельно открывает новые математические истины, которые затем формализуются и проверяются. Результаты опубликованы в открытом доступе вместе с Lean-сертификатами, что позволяет сообществу воспроизводить и развивать их. Такой подход меняет роль ИИ с инструмента поддержки на соавтора научных открытий.

Скептическая оценка маркетинга OpenAI: результаты — не фундаментальный прорыв, а эффективный перебор известных методов без новой математики. AI не обладает интуицией, не формулирует гипотезы, но превосходит людей в рутинном вычислительном переборе, превращая доказательства в вычислительные задачи. Стоимость $2000 вводит в заблуждение: скрытый масштаб экспериментов (p-value hacking) и низкая загрузка мощностей искажают реальную цену. Отсутствует прозрачность: неизвестно число попыток, объяснения содержат логические скачки, затрудняющие проверку. Lean-доказательства достигают 50k строк, но стиль изложения слаб. Настоящий прорыв наступит, когда AI создаст новую ветвь математики — пока лишь усиливает внимание к существующим областям. Ускорение решения задачи ближайшего вектора угрожает криптографии, что уже учитывается переходом на гибридные схемы. Практического применения в медицине или материаловедении пока нет. Тревога по поводу разрушения академической системы: если AI решит задачи, лежащие в основе научных карьер, это подорвёт финансирование и престиж. Ирония: заявление OpenAI о «ответственности за корректность» доказательств сравнивают с добровольным статусом козла отпущения.

Нейросимволический синтез программ позволяет создавать надёжные и интерпретируемые системы рассуждений, объединяя нейросетевые подходы с символической логикой. Метод генерирует формальные доказательства для каждого шага рассуждения, что обеспечивает прозрачность и проверяемость результатов, критически важные для таких областей, как автоматизированное доказательство теорем и объяснимый ИИ.

Технология демонстрирует повышенную устойчивость к ошибкам и способность работать со сложными логическими структурами, избегая "галлюцинаций", характерных для чисто нейросетевых моделей. Практическое применение включает автоматизацию рассуждений в математике, верификацию программного кода и создание систем, требующих чёткой аргументации.

• Обсуждение фокусируется на гибридном подходе, сочетающем языковые модели (LLM) для генерации структурированных предположений (например, на JSON DSL или в логических синтаксисах, таких как SMT, Prolog) и последующей верификации этих выводов с помощью детерминированных решателей (таких как Z3) или теорем-проверов (как Lean).
• Участники подчеркивают как потенциал этого подхода для повышения надежности и интерпретируемости рассуждений ИИ, так и его фундаментальные ограничения, такие как «проблема автоформализации» (autoformalization gap) — риск того, что LLM некорректно переведет запрос в формальную логику, что приведет к принципу «мусор на входе — мусор на выходе».
• Приводятся практические примеры применения метода, включая проверку согласованности бизнес-политик, автоматизацию математических вычислений (например, с помощью SymPy) и синтез программ.
• Высказываются критические замечания о природе LLM: они не являются «мыслящими» системами, а лишь статистическими моделями, генерирующими правдоподобные шаблоны, и их вывод принципиально не детерминирован и может быть неполным или ошибочным.
• Обсуждаются технические детали и улучшения, такие как использование структурированных выходов API, ограниченное декодирование для повышения надежности генерации кода и необходимость более четких примеров в документации проектов.

Теренс Тао делится предварительными соображениями о текущих усилиях по формализации математики с использованием ИИ и языковых моделей. Он отмечает, что хотя автоматизированные системы доказательств, такие как Lean, уже способны проверять сложные математические утверждения, генерация оригинальных доказательств и интуитивных идей остаётся сложной задачей. Тао подчёркивает важность симбиоза между человеческой креативностью и машинной точностью, где ИИ помогает устранять ошибки и предлагает возможные пути решения, но ключевые прорывы по-прежнему исходят от математиков.

Он также указывает на практические ограничения: текущие ИИ-инструменты часто требуют значительной ручной настройки и могут генерировать избыточные или неэффективные доказательства. Однако их способность быстро перебирать огромное количество вариантов делает их незаменимыми помощниками в проверке гипотез и поиске контрпримеров. Тао ожидает, что по мере развития моделей они станут более интегрированными в исследовательский процесс, сокращая время на рутинные проверки и позволяя учёным сосредоточиться на глубинных вопросах.

• Упадок малых организаций и локальных сообществ из-за экономических изменений, включая рост двухдоходных семей и снижение волонтерства.
• Консолидация рынков в пользу крупных корпораций, подкрепленная регуляторными рамками и финансовыми стимулами, ограничивающими малый бизнес.
• Технологии и интернет одновременно упростили создание онлайн-сообществ, но также способствовали росту крупных платформ и снижению локальной активности.
• Социальные последствия: потеря чувства общности, статуса в сообществе и роста ощущения изоляции и бессмысленности у индивидуумов.
• Возможности для возрождения малых организаций через низкие барьеры входа в цифровую эпоху и осознание их ценности для общества.