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
8 votes
1 answer
125 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 ...
Dustin G. Mixon's user avatar
7 votes
1 answer
811 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 ...
Jason Rute's user avatar
  • 8,825
1 vote
1 answer
266 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 ...
Charlie Parker's user avatar