Как лучше преобразовать программу на rocq или аналоге в pdf — документ с математическими символами, а не кодом?

По вводным: цель: выполнить следующий алгоритм многократно:

1. По вводным: оформить какое-либо математическое решение/доказательство в инструменте интерактивного доказательства теорем (например, roqc/coq, lean, или ином).
2. По вводным: каким-нибудь автоматическим программным средством (например, coqdoc) преобразовать его в latex, odt или word документ, содержащий привычные математические символы без синтаксиса данного инструмента интерактивного доказательства теорем.

По вводным: таким образом, должна получиться максимально:

• Детальная и понятная
• Точная
• Корректная

Сейчас ситуация такая: математическая документация с минимальным использованием натурального языка (если вдруг этого не избежать, им должен быть русский язык).
Сейчас ситуация такая: на данный момент ни один инструмент интерактивного доказательства теорем не выучил, так как нужно выбрать именно тот, с которым можно будет действовать по вышеописанному алгоритму.
По вводным: знаю python. То есть если существует решение, которое потребует использование какой-нибудь его библиотеки (например, Pytanque, которая подходит для коммуникации с Rocq/Coq), то такое решение тоже подойдёт.

По вводным: таким образом, мои вопросы:
По вводным: для достижения вышеописанной цели:

1. Какое сочетание
   • По вводным: инструмент интерактивного доказательства теорем
   • По вводным: программное средство для автоматического получения документации, соответствующей вышеописанным критериям

   Выбрать?

2. Каким способом именно его использовать (какую команду ввести/куда нажать), чтобы заработало?

По вводным: для информации: coqdoc у меня работает без ошибок, но возвращает вот такой вот документ: