Человек — директор, ИИ — исполнитель: теорему доказали за неделю
Математик Джозеф Миллер формализовал сложный результат из математической физики в Lean 4 примерно за месяц — и сам не написал ни одного доказательства. Всё исполнял ИИ-агент под его руководством.