This feels like the types programming vs. none typed programming.

There are efforts in math to build "enterprise" reasoning systems. For these it makes sense to have a universal notation system (Lean, Coq, the likes).

But for a personal exploration, it might be better to just jam in whatever.

My personal strife in this space is more on teaching: Taking algebra classes, etc. where the teacher is not consistent nor honest about the personal decision and preference they have on notation - I became significantly better at math when I started studying type theory and theory of mechanical proofs.