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 bo

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