I have a pet (undergraduate complex analysis) formalisation project in Lean, purely for didactic and recreational purposes. I find it rewarding in the same way

I have a pet (undergraduate complex analysis) formalisation project in Lean, purely for didactic and recreational purposes. I find it rewarding in the same way others may find it rewarding to train for a triathlon - it's often extremely grueling work and it can take forever to make even modest progress. When I actually do get to a "big" result such as defining pi (from scratch) or Cauchy's integral theorem it feels rewarding, but there's a ton of torn out hairs along the way, when linarith is stupider than it should be, I need to spend forever to prove very obvious things, I can't find the tactic I need in mathlib or I realise there's barely anything about triangles in there. For somebody like me without a PhD it also doesn't help that mathlib almost always goes for full generality which makes it hard to use it effectively (although I do understand the reason for it). I think this is all very exciting but I also think ergonomics will probably need to improve quite a bit before Lean will become mainstream in mathematics.