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