Lean (and iirc Mathematica) use backslash escapes: you type \symbolname and the symbol is inserted by your editor.
You can also imbue the backslash escape sequence with the same meaning as the unicode, so that in the event that the editor didn’t make this replacement it would still mean the same thing.
julia also. Mathematica uses literal “escape” sequences, ie you start a symbol by pressing the esc key and finish with another esc (aside from a bunch of bindings for commonly used things).
https://xpqz.github.io/learnapl/intro.html