Comment by ratmice

Opinion, but lean and coq both use dependant type theory, while isabelle uses a first order logic. Between coq and lean, lean has always had great support for unicode, where coq always seemed to me ascii first, and coq itself predates the publishing of the unicode standard and formation of the unicode consortium. At least my feeling has always been that syntax probably takes no small part in it. Because with lean one can use all the familiar mathematical alphanumeric symbols and operators.