Portnov писал(а):
Значит, надо отдельно доказывать корректность программы, составляющей доказательства…
Наверное, проще написать отдельную программу, только
проверяющую доказательства, записанные на входном языке этой программы. И доказать её корректность.