Понятно, что доказать любое наперед заданное утверждение алгоритмически нельзя. А вот проверить полученное тем или иным образом - или опровергнуть, что важнее для приложений - почему бы и нет?

Предположим, что доказательство формализовано тем или иным образом. Тогда можно построить такую метафору: док-во <-> программа, система проверки <-> компилятор. Что указывает на ошибочность док-ва (на метауровне, грамматические ошибки исключаем): использование недоказанных утверждений <-> обращение к несуществующим библиотекам, нарушение правил логического вывода <-> неправильный вызов функций и т.д.