[cwzwarich]

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

[a1o]

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

[denotational]

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...

[a1o]

Thank you!