De Mora built Lean to verify software correctness more expressively than Z3, and mathematicians later adopted it, bringing an interactive theorem prover into more mainstream mathematical practice for the first time.

“Uh, it makes it a much more powerful thing. So what my book is, is ultimately the story of how Lean, this interactive theorem prover that de Mora builds to verify the correctness of software programs in a richer way than he could with Z3. gets, in a sense, co-opted by mathematicians who see the potential in it, and for the first time an ITP breaks through into a more mainstream way of working at math.”