[robinzfc]

Isabelle is a generic theorem prover. It supports the standard set theory on first order logic as well, but it's most popular logic is HOL, which is a kind of type theory. Isabelle is well integrated with LaTeX, so its support for mathematical symbols goes beyond unicode. One can write complete well typeset mathematical papers inside Isabelle, and people do. So it's not that. Yet, the dynamics of Lean uptake among mathematicians is much better, so I am curious why is that. I would really like to see an opinion of someone who knows both Lean and Isabelle well, but prefers Lean for formalized mathematics. Or is that all coincidence and hype?

[ratmice]

I am talking not about the ability to typeset your proofs, but the source code itself for the proofs. At the very least all the Isabelle and Coq proofs I've looked at have look much more like source code than the proofs they formalize.