There are formal grammars. The formal grammars are really hard to understand in my humble opinion. The best examples I think are COQ (see e.g. https://en.wikipedia.org/wiki/Coq) and Lean (see e.g https://en.wikipedia.org/wiki/Lean_(proof_assistant) ).

Yes, we are too lazy to be 100% formal and many times we are too lazy to be mostly formal. This is mostly because we target our writing to other mathematicians who have no need to see every small step and including every step makes the proofs long. On the other hand, I do feel that generally speaking mathematicians should show more of their work and skip fewer steps.

I find your statement "People can't be bothered to be exact about things because being exact is hard and people avoid hard work." to be very true. Being precise is difficult.