Sure, he is one of biggest advocates for it, and yet he was quite clear that it is not yet possible for him to do his actual research in Lean.

Quoting one of the recent papers (2020):

> With current technology, it would take many person-decades to formalise Scholze’s results. Indeed, even stating Scholze’s theorems would be an achievement. Before that, one has of course to formalise the definition of a perfectoid space, and this is what we have done, using the Lean theorem prover.