Why do proof authors use natural language sentences to write proofs? I haven't read very many proofs. The majority of the ones that I've read, I've read in my first-year proofs textbook. Nevertheless, its first chapter expatiates on the proper use of English in mathematical proofs, so I suspect that most proof authors do use both English (or another natural language) and formal proof systems for writing their proofs. However, I can't imagine many circumstances where mathematical notation and a formal proof system wouldn't suffice to convey the author's pertinent thoughts. 
I suspect that proof authors have good reasons for making use of both English and formal expressions in their proofs, but I can't think of what those reasons are. Why do proof authors use English and formal expressions to write proofs? Are there stylistic rules (or guidelines) that state how, and in what parts of the proof, an author should, and shouldn't, use English? 

You wrote

I can't imagine many circumstances where mathematical notation and a formal proof system wouldn't suffice to convey the author's pertinent thoughts.

The case is, mathematical proofs contain lot of hand-waving argument such as referring to symmetry or to consistent change of variables. Editors are eager to accept these arguments but theorem provers are not. The formalisation of such arguments is an active area of research. One example is nominal sets which develops a full algebraic theory of the mentioned change of variables. It has an implementation in the Isabelle theorem prover called Nominal Isabelle and it requires some work to use.
There is a vast literature on what a proof is, a good place to start is the paper Social Processes and Proofs of Theorems and Programs.
