In summer 2013, Leo told Jeremy by email that he had decided to adopt dependent type theory for Lean.

“But ultimately, Leo emails Jeremy back during that summer of 2013 and tells him, "I've decided to go with dependent type theory," and Jeremy basically does a dance at home in Pittsburgh because he just knows the, the seeds are there now for Lean to be useful in math in the way he's always wanted an interactive theorem prover to potentially be useful.”