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-pr...