← Back to context Comment by adamnemecek 1 year ago What was the tipping point that made you want to work on Lean? 4 comments adamnemecek Reply cwzwarich 1 year ago 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 1 year ago How does Lean compares with Coq? (I am not familiar with Lean but am familiar with Coq) denotational 1 year ago 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... 1 reply →
cwzwarich 1 year ago 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 1 year ago How does Lean compares with Coq? (I am not familiar with Lean but am familiar with Coq) denotational 1 year ago 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... 1 reply →
a1o 1 year ago How does Lean compares with Coq? (I am not familiar with Lean but am familiar with Coq) denotational 1 year ago 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... 1 reply →
denotational 1 year ago 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... 1 reply →
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...
1 reply →