Math papers can be pretty sloppy, and you don't realize this until you start working with formal mathematics—then it's obvious. Almost all hand "proofs" in mat

Math papers can be pretty sloppy, and you don't realize this until you start working with formal mathematics—then it's obvious. Almost all hand "proofs" in math papers have minor bugs, even if they're mostly correct in the big picture sense. Even math designed to support programming (e.g. in computer graphics) is almost always incomplete/outright wrong in some meaningful way.* But with a struggle, it's still largely usable/useful. I've used advanced mathematics most of my career to do work (i.e. read a paper, implement it), but the ability to actually use math to do new things in computer science that mattered only to me only happened after I learned TLA+, which took a few weeks of solid study to click. Since then, it's been a pleasure. My specs have never been this good! Lamport's video course on TLA+ is pretty good, but honestly I've read everything I can find on the topic so it's difficult to know what helped me the most. *I think this is because, short of doing formal mathematics, there's no way to "test" your math. It's the equivalent of expecting programmers to write correct code the first time with no tests, and without even running the code.