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

Question

[mr_secret]

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

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

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

• детальная и понятная
  
• точная
  
• корректная
  

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

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

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

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

Comments

[Василий Банников]

Зачем вам интерактивное доказательство, если вы собираетесь писать статьи в журнал?
Пишите руками - это даже легче будет, так как можно будет человеческим языком описывать то что нужно.
Если нужны формальные доказательства, то зачем вам тогда pdf, если все эти теоремы должны гоняться на исходниках?

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

[mr_secret]

Василий Банников, в моём ВУЗе нужно сдавать работы по математическим предметам в pdf, однако, когда я сдаю их, я хочу быть уверенным, что моё решение/доказательство абсолютно корректно, чтобы проверяющие не могли поставить мне балл ниже максимального.

[Василий Банников]

mr_secret,
1. Попробуй прямо спросить препода, будет ли он принимать подобную работу - может он согласиться в принципе взять исходник с доказательством на coq.
2. В чём трудность руками перевести корректное доказательство на человеческий язык?

[mr_secret]

Василий Банников,

1. Попробую, но скорее всего он не согласится принимать код на roqc. К тому же в течение семестров будет несколько математических предметов, и каждый самостоятельно будет утверждать политику в отношении данного вопроса: то есть, даже если сейчас разрешат, вообще не факт, что будут разрешать потом.
   
2. Тут есть не трудность, а стремление избежать человеческого фактора при переводе содержимого из кода на roqc в pdf. +экономия времени
   

[mr_secret]

Василий Банников,

Попробуй прямо спросить препода, будет ли он принимать подобную работу

а он не сможет не принять, так как pdf есть официально утверждённый формат сдачи работ

[Василий Банников]

mr_secret, если внутри ересь, которая не имеет отношения к предмету и задаче, то тогда конечно примет, но сразу неуд/незачёт пропишет и скажет переделывать)

[Василий Банников]

mr_secret,

Тут есть не трудность, а стремление избежать человеческого фактора при переводе содержимого из кода на roqc в pdf. +экономия времени

Формальные доказательства точно не про экономию времени) Пиши сразу на человеческом. Если будет ошибка в доказательстве - будет хорошо, если бы узнаешь об этом, ибо это значит что голова не так настроена.

Всё равно доказательства на формальном языке требуют освоения сразу двух навыков:
1. Умения сформулировать доказательство в голове
2. Умение перевести его на язык машины

[mr_secret]

есть наводка https://github.com/cpitclaudel/alectryon
но мне не удалось заставить работать эту библиотеку, чтобы запустить и проверить: является ли она ответом на вопрос