Jeremy believed dependent type theory gave Lean the potential to support mathematics as he had long wanted an interactive theorem prover to do.

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