It's called "learning a new language". You know what you want to express - you don't know how to express it in a way that your interlocutor will understand. W

It's called "learning a new language". You know what you want to express - you don't know how to express it in a way that your interlocutor will understand. Whether your interlocutor is a computer speaking Lean, or a human speaking your non-native tongue. All the benefits are on the other side of the learning curve.