Если я правильно понимаю, это означает, что на первый план выходит как раз проблема формализации, т.е. что Lean-формулировка теоремы соответствует исходной, и эта проблема перевода, в частности, сложнее проблемы останова МТ.
Нет, про неразрешимость там другое (и ИМХО довольно бессмысленное). Если, например, в тексте говорится "пусть
- минимальное число такое что
", то формализация должна доказать его существование. А это в общем случае неразрешимая задача.
И там поднимается еще один момент: как правило, доказательство больших результатов разбито на части, и потом часто эти части переиспользуются отдельно. При автоформализации модель может легко поменять промежуточные рассуждения, и какие-то из промежуточных лемм вообще не доказать - так что наличие перевода опубликованного доказательства в Lean гарантирует только доказуемость исходного утверждения (по модулю багов и ошибок в его формализации - но последним как раз должны заниматься люди), но не правильность доказательства.
