I don't think there was a single tipping point, just a growing accumulation of factors:

- the release of Lean 4 slightly over a year ago, which impressed me both as a proof assistant and a programming language

- the rapid progress in formalization of mathematics from 2017 onward, almost all of which was happening in Lean

- the growing relevance of formal reasoning in the wake of improvements in AI

- seeing Lean's potential (a lot of which is not yet realized) for SW verification (especially of SW itself written in Lean)

- the establishment of the Lean FRO at the right time, intersecting all of the above

How does Lean compares with Coq? (I am not familiar with Lean but am familiar with Coq)

Mario Carneiro’s MS Thesis has a good overview of the type theory and how it compares to Coq: https://github.com/digama0/lean-type-theory/releases/downloa...

Thank you!