Questions tagged [translating]
Converting from one form to another. Such as converting a proof from a logic based framework to a dependent type framework.
5 questions
10
votes
1
answer
1k
views
What is a deep embedding vs a shallow embedding? With examples?
I'm unclear on the terms "deep embedding" and "shallow embedding". I understand they are concerned with using one logic inside another, e.g. using Metamath/set.mm proofs in Lean ...
- 10.3k
3
votes
1
answer
403
views
How does one translate Lean to Coq (and visa versa)?
I am interested in translated Lean to Coq and visa versa. One first reason is because I want to translate the miniF2F data set in Lean to Coq but lack the expertise to do it. Though in general I'd ...
- 383
8
votes
1
answer
133
views
Have the common algorithms in existing computer-assisted proofs been transitioned to proof assistants?
In my experience, one of the most common applications of computer-assisted proofs in math is establishing that a given system of constraints is infeasible. Here are some examples of settings and tools ...
- 981
9
votes
0
answers
142
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 ...
- 373
23
votes
7
answers
1k
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.
- 1,348