Хз Мартин Клеппманн говорит что сможет, но у меня сомнения.

По тому что читал, с пруверами основная проблема для ллм
разбиение промта (софта) на лемми, для котрих можно подобрать елементарних доказательства
на основе корпуса мзвестних лемм.

А такое разбиение ето в общем случае np-hard задача, рандомизатор с поиском даже
если ето монтекарло поиск вряд ли сможет его хорошо делать.

Зато когда человек уже все разбил на лемми, с написаним скриптов ллмки справляются хорошо,
так что поможет оно точно заиметь больше пруфов.