🧠 Claude доказал, что 67,2% нулей дзета-функции лежат на прямой Никакой гипотезы Римана ИИ не доказал — премия Клэя на месте, ажиотаж в заголовках — преувеличение. Реальный результат жёстче и интереснее: невыпущенная исследовательская версия Claude от Anthropic за полтора суток работы подняла планку доказанной доли нулей на критической прямой с 41,66% до 67,2%. Предыдущие рекорды с 1974 года шли методом Левинсона, и каждый следующий процент давался годами изощрённых комбинаторных выкладок. Claude пошёл другим путём — возродил парную корреляцию Монтгомери, подход, который требовал гипотезы Римана как условия; ИИ обошёл это ограничение через недавнюю безусловную теорему о парной корреляции. Вычисления заняли 31 миллион выходных токенов и 2400 команд оболочки, распределённых между ~60 подчинёнными агентами, а итоговое доказательство проверено в Lean 4 — все теоремы успешно собираются. Имена людей в препринте — математики Левент Альпёге и Ральф Фурман, формализатор Эрик Изли и постановщик задачи Джаред Самнер, а также внешняя проверка Брайана Конри и Дэниела Голдстона. Первоисточник — подробный разбор на Habr. 60 подчинённых агентов — это иерархия, и вопрос не в том, выдумала ли модель что-то, а в том, на каком именно шаге это могло произойти до того, как попало под проверку Lean. Формальная проверка ловит ошибки на выходе, но не в процессе рассуждения — и зазор между «что модель думала» и «что успешно собралось» в статье не измерен. Кто-то уже пробовал воспроизвести такой процесс на открытых моделях? #Claude #Anthropic #нейроматематика #Lean4 #формальнаяверификация