In addition to formalising _theorems_, one can aim to formalise _definitions_. See here for some discussion: https://mathoverflow.net/questions/311071/which-ma

In addition to formalising _theorems_, one can aim to formalise _definitions_. See here for some discussion: https://mathoverflow.net/questions/311071/which-mathematical-definitions-should-be-formalised-in-lean https://mathoverflow.net/questions/311071/which-mathematical... Of course the two are very much intertwined but I think if we're to get serious about formalising mathematics, it would be better to aim to have fully formalised statements of major theorems rather than their proofs for now.