Skip to main content

Questions tagged [translating]

Converting from one form to another. Such as converting a proof from a logic based framework to a dependent type framework.

Filter by
Sorted by
Tagged with
23 votes
7 answers
996 views

Is there a way to automatically translate proofs from one proof assistant to another?

Is there any way to easily translate proofs from one proof assistant to another? If so, how does it work? Credit to: Kevin Buzzard's question.
taylor.2317's user avatar
  • 1,338
9 votes
0 answers
132 views

Has there been any work on automated translation of tactic proofs to everyday language?

There are times when I've completed a proof with a lot of backwards reasoning, and I've kind of lost the thread of what I've actually done. It would be nice if there was something that could ...
march's user avatar
  • 373