Рой агентов формализовал классификацию конечных простых групп за 24 дня: узким местом стала проверка, а не генерация

Проект Axiom завершил полную формализацию классификации конечных простых групп в Lean за 24 дня с использованием роя из десятков агентов. Основной проблемой стала не скорость создания доказательств, а пропускная способность системы верификации и необходимость удаления ложных допущений, принятых агентами для ускорения работы.