I don’t know about their motivation, but I would say mine is that Lean is a real programming language. Coq is not really meant for “prosaic” programming, more’s the pity.
Lean is also a lot faster.
No specific motivation tbh. I did the number theory game on the recommendation of a friend and found it fun. Made me think.
What does the real programming language part help in? Developing tactics? Or is it because even when you are typing the "math parts" it corresponds to a real programming language giving you a nicer mental model?
Because from what I understand Rocq too has Gallina or something right?
I guess my other point is Rocq seems to have a lot of textbooks too so I was wondering which one to read about when I get some more time - Rocq or Lean.
>Lean is also a lot faster.
What do you base that on? I don't think I've seen a performance comparison but I'm not great at internet searches.