It is weird to be honest. I first learned Coq and then started taking upper level maths classes. My group theory proofs were panned by my TAs as overly verbose, very precise, and I was specializing on H_1 and H_2s everywhere and having IHns flying around like crazy because I could not fathom how one proves things without formally connecting things up.
Then my profs told me I was not “wrong”, but proofs or expositions are to most mathematicians not programs (ha! How did I not know. You teach me natural deduction and expect me not to program?), more like convincing arguments/prose. At some point one abstracts.
Humans, even talented mathematicians, have limited context. A big part of any mathematics text is abstraction for the sake of understanding. It can be confusing at first, but once you learn how to read mathematics with these abstractions in place, reading everything spelled out with great verbocity and pedantic accuracy is frustrating and tiring. You're forcing your eyes to parse and interpret a whole bunch of symbols that your brain doesn't need.
Of course, some mathematicians take it too far and use these abstractions to obfuscate and prove how smart they are. Like everything, it's a balance.
I personally wasn't a fan of this particular shorthand when I read this book but I got used to it quickly.
Comments
It is weird to be honest. I first learned Coq and then started taking upper level maths classes. My group theory proofs were panned by my TAs as overly verbose, very precise, and I was specializing on H_1 and H_2s everywhere and having IHns flying around like crazy because I could not fathom how one proves things without formally connecting things up.
Then my profs told me I was not “wrong”, but proofs or expositions are to most mathematicians not programs (ha! How did I not know. You teach me natural deduction and expect me not to program?), more like convincing arguments/prose. At some point one abstracts.
Humans, even talented mathematicians, have limited context. A big part of any mathematics text is abstraction for the sake of understanding. It can be confusing at first, but once you learn how to read mathematics with these abstractions in place, reading everything spelled out with great verbocity and pedantic accuracy is frustrating and tiring. You're forcing your eyes to parse and interpret a whole bunch of symbols that your brain doesn't need.
Of course, some mathematicians take it too far and use these abstractions to obfuscate and prove how smart they are. Like everything, it's a balance.
I personally wasn't a fan of this particular shorthand when I read this book but I got used to it quickly.