Тихо-тихо, а ИИ создаёт инфраструктуру математики

Сейчас в математике происходят реально интересные времена, и речь не об открытиях, а о простых, но важных вещах.

Так команда из Meta(запрещена в России) и французских институтов с помощью ~30 000 агентов Claude за 1 неделю полностью формализовала в Lean 500-страничный учебник по алгебраической комбинаторике.

Вся эта работа обошлась ~ $100 000, авторы пишут, что после устранения неэффективностей в оркестрации можно снизить цену в 3–10 раз даже без более сильных моделей.

Уже сейчас это сопоставимо с зарплатами команды из людей - экспертов.

В будущем эта работа полезна не только математикам, но и для:

• железа,
• операционных систем,
• баз данных,
• GPU-ядер,
• компиляторов и тд.

GitHub