Operator algebras, and functional analysis more generally, is still in early stages with regards to formalization. In some aspects we have made reasonable progress, but in others we are stymied by various obstacles. We will highlight some of these successes and difficulties and discuss how we might turn these into opportunities to improve the library, especially places where bespoke tactics may be particularly effective.