Как я написал выше анониму, с моей досужей точки зрения - основное отличие в мощности "движухи" (community) и богатстве / динамике расширения mathlib (что, собственно, двигает в сторону удобства). Боковое рассмотрение (чисто спекулятивное) - выбор молодого специалиста в пользу Lean может быть обсуловлен бОльшими возможностями получить зачёт, написать статью - в сравнении с Coq, с которым делали (и, может, продолжают делать) статьи формализаторы старшего поколения. Чёткая поколенческая отсечка. Кстати, просмотрел заметку computer scientist-а, в которой он аргументировал свой выбор для работы с алгоритмами в пользу Coq, сравнивая с Lean и Isabelle - https://ntietz.com/blog/first-impressions-of-lean-and-coq/ (на случай, если вам будет интересно просмотреть; я так и не знаю, кто вы по профессии - я вот - программист).