Ограниченный компиляторно-управляемый ремонт улучшает поиск доказательств на уровне тактик в Lean 4
В статье предложён ограниченный онлайн‑модуль пошагового ремонта: при выборе K кандидатных тактик и отклонении тактики компиляторный текст ошибки передаётся предобученной модели ремонта, которая пытается исправить шаг до R раз на месте. На подмножестве из 1 990 теорем бенчмарка LeanDojo метод даёт до 32% относительного прироста (ещё 82 решённые теоремы) при разных K∈{1,3,5,8}, успешно воспроизводится на Lean Workbook (почти удваивает solve rate) и приносит выгоду главным образом для мелких ошибок выполнения тактик при предсказуемом увеличении времени работы.