✔️ ИИ за 24 дня формализовал самое длинное доказательство в истории математики, над которым около 100 учёных работали десятилетиями. Компания Axiom Math объявила о завершении компьютерной проверки теоремы классификации конечных простых групп (CFSG), известной как «Огромная теорема». Оригинальное доказательство занимает 15 000 страниц в более чем 500 научных статьях. О чём вообще теорема? Представьте куб. Его можно повернуть 24 способами так, чтобы он выглядел точно так же. Эти преобразования образуют математическую группу. Теорема классифицирует фундаментальные «строительные блоки», из которых состоят все конечные группы симметрий. Это своеобразная периодическая таблица симметрий, применяемая в алгебре, теории чисел и математической физике. Что сделал ИИ: За 24 дня десятки ИИ-агентов создали около 43,1 млн строк кода на Lean. Формализовали доказательство, которое математики собирали на протяжении десятилетий. Обнаружили 34 существенных расхождения с опубликованными математическими работами. Нашли контрпримеры к некоторым утверждениям и разработали альтернативные доказательства. Получили новый результат в теории групп, необходимый для выбранного пути доказательства. В отдельных случаях ИИ обнаружил ошибки в исходных рассуждениях и построил новые математические аргументы, чтобы их исправить. Работа велась совместно с математиками, включая специалистов, участвовавших в первоначальной классификации. Результат Axiom представляет как первое полное доказательство CFSG, проверяемое компьютером. Код и материалы открыты для независимого изучения. Это пример того, как ИИ-агенты могут не только ускорять математическую работу, но и проверять фундаментальные результаты, которые раньше было практически невозможно перепроверить целиком. https://axiommath.ai/research/the-enormous-theorem-formalized/ @ai_machinelearning_big_data

📚️️️️️️ ИИ самостоятельно нашёл и доказал новые математические закономерности Исследователи Google DeepMind и Кембриджа создали агента на базе Gemini, который обнаружил точные правила поведения 11 машин Тьюринга на границе задачи Busy Beaver. Машина Тьюринга - простейшая модель компьютера. Даже программа с шестью состояниями может вести себя настолько сложно, что неизвестно, остановится ли она вообще. Агент искал закономерности в работе таких программ, формулировал гипотезы и строил доказательства. Затем проверял их в Lean — системе, которая строго проверяет математические рассуждения. Результат - компактные правила, позволяющие описывать сразу множество шагов программы вместо пошагового перебора. Остановятся ли эти 11 машин, пока неизвестно. Но теперь их поведение получило точное математическое описание. Это шаг к ИИ, который самостоятельно находит предмет для исследования и доводит гипотезу до проверенного результата. https://arxiv.org/abs/2610.22603

🧮 Большую часть математики можно формализовать за три года. Но что мы получим на выходе? Такую перспективу описывают Кевин Баззард, Джереми Авигад и другие математики в блоге Xena. Формализовать - значит перевести определения, теоремы и доказательства на язык вроде Lean, чтобы компьютер мог проверять логические шаги. Авторы видят в ИИ возможность резко ускорить эту работу. Но предупреждают: миллионы строк проверенного кода могут оказаться бесполезными, если на них невозможно строить новые исследования. Нужны понятные определения, документация, совместимость библиотек и повторное использование результатов. Уже есть два подхода: • Tau Ceti - единая библиотека: математики задают план, ИИ пишет код, другие ИИ проверяют. • Formal Frontier - система агентов, превращающая математические тексты в связанные формальные библиотеки. Компьютерная проверка доказывает корректность формального утверждения. Ценность для науки появляется, когда результат можно понять, исследовать и использовать дальше. 📖 https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/

Навье — Стокс, упаковка сфер и Lean: как ИИ пришёл в большую математику Как уложить одинаковые шары максимально плотно? С апельсинами на прилавке всё кажется очевидным. А вот доказательство оптимальной упаковки в восьми измерениях появилось только в 2016 году. Спустя десять лет ИИ-агент Gauss помог завершить перевод этого доказательства на формальный язык Lean. Правда, к тому моменту люди уже проделали огромную подготовительную работу. А в сентябре 2026 года OpenAI объявила, что её новая модель решила задачу тысячелетия Навье — Стокса. Здесь речь уже идёт о поиске ранее неизвестного доказательства, а не формализации готового. Заявление вызвало немало вопросов, в том числе о корректности результата и степени самостоятельности ИИ. И это уже совсем другая история.

Возвращаясь к математике, я прочитал разные мнение, и одним из самых откликнувшихся оказался блог «To grieve, or not to grieve?» от Kevin Buzzard, основателем проекта Xena, цель которого — оцифровать всю современную математику, переводя теоремы и доказательства с человеческого языка на Lean. Хоть он и не является основателем Lean, он активный контрибьютор, и именно в рамках Xena делается библиотека примитивов mathlib для Lean, на которую можно опираться при составлении своих доказательств. Kevin описывает 5 классических стадий принятия, и подмечает, что сейчас разные математики находятся на разных уровнях: — кто-то, например та самая «организация людей-математиков», находится в отрицании — кто-то пытается торговаться, например, группа математиков, которые «дают рекомендации» OpenAI (но те не обязаны их соблюдать). Они тоже не рады слоп-дропу 700+ статей, и ратовали за другой подход, хотя в целом понимают, что с AI математика теперь уже навсегда. — многие пост-доки и PhD в депрессии Профессор Buzzard задаётся филосовским вопросом: а зачем мы вообще занимаемся математикой? «Думаю, несколько лет назад многие математики с радостью согласились бы с тем, что математическое сообщество вручает самые престижные премии и награды тем, кто доказывает самые сложные теоремы. Однако теперь, когда сложные теоремы доказывает ИИ, мы, похоже, тратим много времени на объяснение того, что на самом деле эти награды и премии вручаются тем, чьи идеи позволяют нам глубже понять нашу область науки». Часто цитируют эссе 1994 года «О доказательстве и прогрессе в математике», где выражается мнение, что «дело не в количестве теорем, а в человеческом понимании» — эта цитата даже висит на картинке в шапке блога Terence Tao. Но дальше Kevin приводит личный пример, когда во время работы над докторской руководитель советовал ему не разбираться в одной из ключевых работ, потому что тот не успел бы и копнуть глубоко, и написать докторскую. Kevin признается, что он до сих пор так и не вернулся к той теореме — так «понимает» ли он свою работу? А кто понимает доказательство Великой Теоремы Ферма? Сам Kevin понимает лишь узкую часть того доказательства, потому что полное решение безумно сложно и требует невероятной ширины знаний — хотя он по теме Великой Теоремы Ферма читал блок лекций. Тут я от себя добавлю, что многие результаты ИИ как раз и приходятся на стыки нескольких направлений, и что часто один человек просто не может преуспеть и там, и там, чтобы прийти к открытию. Поэтому и полноценная человеческая проверка самых значимых работ, опубликованных OpenAI, может занять ОЧЕНЬ много времени.

10 агентов Opus 5.5 за 15 часов обнаружили алгоритм поиска кратчайшего пути, превосходящий Дейкстру Поиск кратчайшего пути – классическая проблема теории графов, на решении которой основываются навигаторы, роутинг в интернете, логистика и куча других задач современного мира. В 1959 году нидерландский информатик Эдсгер Дейкстра предложил для поиска кратчайшего пути алгоритм O(m + n log n), который следующие 65 лет оставался золотым стандартом и использовался буквально везде. В 2025-м команда из Цинхуа, Стэнфорда и Института Макса Планка впервые обошла его с оценкой O(m log^{2/3} n). Однако выигрыш их решения раскрывается только на достаточно плотных графах (число ребер m ≥ числа вершин n). На разреженных графах Дейкстра все еще был лучше. Vals AI решили потестировать новый Opus 5.5 именно на этом непобитом диапозоне (блогпост). Они запустили 10 агентов, дали им задачу и доску объявлений, чтобы те могли обмениваться идеями и кооперироваться. В итоге за 15 часов и 733 сообщений агенты получили алгоритм C-HD и формально его верифицировали. Это первое доказанное улучшение именно в этой разреженной зоне, где лучшим все еще был Дейкстра: при m ≈ n·log^{3/4}n C-HD дает O(n·log^{11/12}n) против O(n log n) у Дейкстры: при n = 2^1000 выигрыш составляет ~1,78х и растет с размером графа. Правда, несмотря на всю мощь того, как это звучит, и на наличие доказательства в Lean, о практическом ускорении речи пока нет, потому что оценки из предыдущего абзаца –асимптотические, а на реальных графах алгоритм пока не бенчмаркали. То есть при n → ∞ одна кривая гарантировано обгонит другую, однако на практике точка перегиба может возникать только при огромных n, и на любом реалистичном графе Дейкстра все еще будет быстрее, даже если у него худшая асимптотика. Так что эту часть еще предстоит проверить.