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.
