[sadfev]

I was wondering about that too. They are perhaps most important tools for both CS and pure mathematics.

It’s very interesting that Lean has exploded in the mathematics community. Kevin Buzzard talks about it a lot, but I haven’t seen a talk which explains why Lean succeeded in creating a gargantuan math library whereas Coq only recently got respectable math library in “MathComp” (I am also including Analysis library).

I would like to know apart from social reasons what technical choices lead to Lean dominating (ordinary/regular/pure) mathematics.

I hear “quotients” but no one actual explains with a concrete example.

[outlace]

I think it all comes down to the aesthetics and user experience. The Lean webpage is inviting and modern. Coq’s website looks like it’s from the 90s. Lean’s integration with Visual Studio Code is clean and user friendly. The language itself is familiar and polished. The imprimatur of a Microsoft team producing Lean being makes it seem more sophisticated.

[maxwells-daemon]

In my experience: one of Lean's main advantages is developer experience. It's convenient by design, with lots of automation to make easy proofs trivial. You do your work in VSCode or Emacs rather than some outdated IDE, and the server mode makes it easy(ish) to integrate with other software.

[sadfev]

I think CoqIDE is great and ProofGeneral (Emacs) is something all Coq experts use.

I have the opposite experience with Lean 4, the VSCode integration is horrid and documentation is awful.

The only good sources are papers for Lean4.

Granted I can go back to Lean3 but why would I?

[outlace]

But Lean4 is in alpha stage and there are no official stable releases yet, of course it's not well-documented nor polished yet. Lean3 works perfectly well and has everything you need.