I may be simplifying things a little but it is two-fold: one Lean lets you call your theorem whatever you want, but if your vocabulary doesn't include the math objects I am interested in, it is unlikely that you said something interesting about them; secondly steps are painfully small in formalized math and even then you have to fight to get Lean not confused about what you are doing (like typeclass inference), so what you can do in three and half hours from a low base is quite bounded.