For this book specifically, I think the reason is just that Lean is the theorem prover he already knows and uses in his own work [1]. Now as to why he picked L

For this book specifically, I think the reason is just that Lean is the theorem prover he already knows and uses in his own work [1]. Now as to why he picked Lean a few years ago as his go-to theorem prover, I do think that would be an interesting backstory. As far as I know he hasn't written anything explicit about it. [1] E.g., https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/ https://terrytao.wordpress.com/2023/11/18/formalizing-the-pr...