✔️ ИИ за 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

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

📌 Palomar - реестр проверенных LEAN-доказательств Последние месяцы доказательства, сгенерированные ИИ, посыпались валом как для новых результатов, так и для старых, причем часть из них формализована на Lean и проверить такой репозиторий непросто, особенно если ты не эксперт. Нужно убедиться: 🟠что заявленные формальные утверждения действительно имеют доказательства, проходящие проверку типов; 🟠что в доказательствах нет жульничества; 🟠что формальные утверждения по смыслу совпадают с тем, что описано словами. Под эту задачу и Теренс Тао запустил Palomar - реестр математики, верифицированной на Lean. Инициативу вырастили Lean FRO и ICARM. Прием заявок уже идет, чтобы в него попасть, в репозитории должно быть три вещи: 🟢challenge file с коротким и читаемым человеком описанием заявленных результатов на Lean; 🟢solution module с доказательством любой длины; 🟢файл formalization.yaml, где те же результаты изложены обычным языком и собраны метаданные и раскрытия. Снимок поданного репозитория проверяют двумя этапами. Сначала инструмент Comparator смотрит, что solution module типизируется и доказывает ровно то, что заявлено в challenge file. После этого языковая модель сверяет, похоже ли неформальное описание в на то, что заявлено формально. Прошел оба - попал в реестр. Принимают формализации и старых результатов, и новых. Кто автор доказательства - человек, ИИ или оба вместе - значения не имеет. @ai_machinelearning_big_data #news #ai #ml