Тихо-тихо, а ИИ создаёт инфраструктуру математики Сейчас в математике происходят реально интересные времена, и речь не об открытиях, а о простых, но важных вещах. Так команда из Meta(запрещена в России) и французских институтов с помощью ~30 000 агентов Claude за 1 неделю полностью формализовала в Lean 500-страничный учебник по алгебраической комбинаторике. Вся эта работа обошлась ~ $100 000, авторы пишут, что после устранения неэффективностей в оркестрации можно снизить цену в 3–10 раз даже без более сильных моделей. Уже сейчас это сопоставимо с зарплатами команды из людей - экспертов. В будущем эта работа полезна не только математикам, но и для: • железа, • операционных систем, • баз данных, • GPU-ядер, • компиляторов и тд. GitHub