Which mathematical definitions should be formalised in Lean?

I thought this mathoverflow post might be of interest to those who mentioned automated theorem proving in discussions on the recent post on the ABC conjecture (https://news.ycombinator.com/item?id=18034714).