1
$\begingroup$

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 like to translate as many theorem/lemma statements (and proofs if possible) in each others language. How does one do this? Are there tools that do this?

One crazy idea I thought was to translate lean statements to SMT format then to Coq -- since hammers often try to translate back their proofs to the proof assistants language. Other more crazy ideas could be using LLMs & perhaps prompting them with example translations.

Any other ideas are welcomed!

$\endgroup$
7
  • 1
    $\begingroup$ There are dedicated common languages like dedukti etc. $\endgroup$
    – Trebor
    Commented Nov 11, 2022 at 6:22
  • $\begingroup$ Some equalities that hold in Lean may not necessarily hold in Coq, there needs to be nontrivial patches $\endgroup$
    – ice1000
    Commented Nov 11, 2022 at 6:44
  • 2
    $\begingroup$ There is a an EU research network, europroofnet.github.io, which addresses the problem of inter-operability. I recommend you have a look at what they (we) are doing. There is quite a bit of focus on Dedukti – that's what I would start with. $\endgroup$ Commented Nov 11, 2022 at 7:36
  • $\begingroup$ There is already this tool which translates Lean proofs to Coq proofs. The two theories are close enough so that's it's basically a transpiling process. You only get the logical content of libraries, though. $\endgroup$ Commented Nov 11, 2022 at 9:04
  • 3
    $\begingroup$ It's one (hard) thing doing a translation, it's a much harder thing to translate idiomatic Lean code into idiomatic Coq code and vice-versa. Or perhaps not, depending on exactly what the subject matter is. $\endgroup$ Commented Nov 11, 2022 at 12:59

1 Answer 1

2
$\begingroup$

First, I think you mean translate from idiomatic Lean to idiomatic Coq. Automatic translations (or transpilations) of code are notorious for being non-idiomatic, and addressing this is certainly an area of academic research.

Second, since you are talking about mini-F2F, I think you are only interested in translating statements, not proofs. That would certainly be easier than translating proofs idiomatically.

It is pretty clear why this would be a challenge when translating from Lean to Coq. Imagine you have a theorem that you as a human are trying to translate. That theorem uses definitions, say the real numbers and some basic operators on the real numbers. One would have to either automatically redefine the Lean definition of the real numbers into Coq, leading to a less useful (and less idiomatic) translation, or maintain an alignment dictionary between Lean and Coq. This later approach is called concept alignment and can get tricky fast, but is likely reasonable for simple definitions.

If you are interested in translating proofs (which you are not, but I'll mention anyway), that gets even more tricky. The library of facts and the library of tactics could be very different at points. This would make it very difficult to automatically get an idiomatic and maintainable proof in the target language (without machine learning). If you don't care about idiomatic proofs, you could transpile the raw kernel proof if the logics are similar enough (or the source logic can be encoded in the target logic), but remember if you care about idiomatic translations of statements where concepts are aligned and you are using the target definition of the concept, then you can't take a Lean proof about the Lean real numbers and expect to automatically get a Coq proof about the Coq real numbers without doing the hard work of showing that the Lean and Coq real numbers (as well as every operator you use in your theorem statement) are isomorphic. This was the challenge that Mario Carnerio had when translating Metamath into Lean. He took the time to map how the Metamath natural numbers and some basic functions and relations on the natural numbers are isomorphic. This allowed him to translate the Metamath proof of Dirichlet's theorem into Lean (again, not an idiomatic proof and it was never put into Lean' library). However, he didn't take the time to do the same for Metamath's prime number theorem proof.

Practically, you could try the tools mentioned in the comments. I think the Coq-Lean-Import is just for kernel level translation and doesn't have concept alignment so it is likely not helpful to you. Dedukti has a concept alignment project called Logipedia. You might want to give it a try. I have no idea if it would be good enough for your purposes, and if the statements would come out looking idiomatic or computer generated.

Also, you mention large pre-trained language models like OpenAI's Codex. A year ago, this would have sounded futuristic, but this year, they are really starting to show promise. The way they work, is that you give Codex a few (maybe 6) examples of the translation you are trying to do, and then feed it the Lean example you want to translate to Coq. I think it would actually do fairly well on mini-F2F. Here is a paper on this, and here is a github repo doing this for human to Lean translation. Of course, there are no guarantees on your translation accuracy.

But honestly, my understanding is that the largest barrier to translating mini-F2F from Lean to Coq is not the amount of work. The mini-F2F people told me it would only take a week for an expert in Coq. The problem I think is there is a lot of uncertainty on how to translate mini-F2F into Coq idiomatically. Coq, unlike Lean, has many libraries of mathematics and it isn't clear which should be used (or maybe even which definition of the reals should be used). These are not things that any automated system can answer. Once these decisions are made, then one can start to automate the translation (or teach someone like your self or an AI how to translate those statement), but not until. I assume decisions like this are usually at the forefront of every translation project and add to the complexity of the project.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.