Remix.run Logo
tossandthrow 8 hours ago

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.

InfinityByTen 5 hours ago | parent [-]

I have to admit that consistency and clarity of thought are often not implied just by the choice of notation and have not seen many books and professors putting effort to emphasize on its importance or even introducing it formally. I've seen cases where people use fancy notation to document topics than how they think about it. It drives me nuts, because the way you tell the story, you hide a lot how you arrived there.

This is why I picked so well on the exposition by Terry Tao. It shows how much clarity of thought he has that he understands the importance of notation.