I have bounced off Lean a few times. What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. I can never seem to get past the "variable is an integer" examples. I realise that the objective in using these tools is exactly the problem in formulating your expression. I think it would be awesome if tools could generate novel mathematics. Where we could express "P=NP" and have computers just churn on that for a few thousand CPU hours.