I asked a similar question in the comments on a youtube video, and Mario Carneiro, one of the people who work on Lean, answered me. He said he does work on thi

I asked a similar question in the comments on a youtube video, and Mario Carneiro, one of the people who work on Lean, answered me. He said he does work on this area, and it kind of works (at least for the theorems you would want to translate?), but in addition to the proofs being very not nice to read, the way the statements of the theorems are translated are, by default, also rather not nice (being statements about specific formulations of the objects (such as the set of integers) as they are expressed/defined in the language being translated from, instead of referring to the corresponding objects that have been defined in the language being translated to. However, he says that it doesn’t take all that much work to manually massage it until the statement of the theorem is expressed in the way that you want it to be. I’m on my phone right now, and the phone youtube app doesn’t give me a permalink, but I’ll try and edit this comment soon on laptop to include link to the comment section. Edit : here are links to what Mario Carneiro said in the thread click the read all replies to read the full thread) https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S8caeH54AaABAg.9-lfXqsNEk29-wEI6kwEni https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S... https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S8caeH54AaABAg.9-lfXqsNEk29-wJfoexc7_ https://www.youtube.com/watch?v=Dp-mQ3HxgDE&lc=UgwpFSmapLZ5S...