Why do proof authors use natural language sentences to write proofs?

An ordinary mathematical proof¹ is a piece of expository prose. Its purpose is to convince the reader that the theorem is true. Obviously it should be mathematically correct and logically sound, but it should also be clear and easy to follow. Writing in (paragraphs of) sentences, and using words for the connective tissue that gives a road map for the logic of the argument, generally makes the prose more readable. By all means use symbols when they’re appropriate: the quadratic formula is much easier to follow when expressed symbolically than when written out in words! But don’t fall into the trap of thinking that the more symbolism you use, the more professional your argument looks.

For an actual (and fairly simple) example you might look at this question and my answer to it.

¹ The word proof is also used for a formal object in mathematical logic. Trying to follow a formal proof is rather like trying to figure out what a computer program does by looking at the machine language.

The following is a purely formal proof of the irrationality of $\sqrt 2$, formalized using the HOL theorem prover Coq. It is equivalent to this human-language proof:

If there is an $n$ such that for some $p$, $n^2 = 2p^2$, then let's take the least positive such $n$ and the corresponding positive $p$, in this case we have (i) $(2p-n)^2=2(n-p)^2$ and (ii) $(2p-n) < n$, thus a contradiction.

Your question should now answer itself.

Require Import ZArith ZArithRing Omega Zwf.
Open Scope Z_scope.

Lemma Zabs_square : forall x, Zabs x ^ 2 = x ^ 2.
intros; case (Zabs_dec x); intros Heq; ring [Heq].
Qed.

Lemma Zabs_st_pos : forall x, x <> 0 -> 0 < Zabs x.
intros; assert (H':= Zabs_pos x); case (Zabs_dec x); intros; omega.
Qed.
Hint Resolve Zabs_pos Zabs_square Zabs_st_pos.

Theorem integer_statement :  ~exists n, exists p, n ^2 = 2* p^2 /\ n <> 0.
intros [n [p [He Hz]]]; pose (q := Zabs n); pose (r :=Zabs p).
assert (H : (0 < q /\ 0 <= r) /\ q ^2 = 2* r ^2).
  assert (F : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs p ^ 2 = p ^ 2 /\
            Zabs n ^ 2 = n ^ 2) by auto.
  destruct F as [H1 [H2 [H3 H4]]];  unfold q, r; split; auto; ring [H3 H4 He].
generalize r H; elim q using (well_founded_ind (Zwf_well_founded 0)); clear.
assert (fact_sq : forall x, x^2=x*x) by (intros; ring).
intros n IHn p [[Hn Hp] Heq].
assert (Hmain_eq: (2*p-n)^2 = 2*(n-p)^2) by ring [Heq].
assert (Hs: 0 < n^2) by (rewrite fact_sq; apply Zmult_lt_0_compat; auto).
assert (Hpn : p < n).
  apply Znot_ge_lt; intros Habs.
  assert (2*p^2 <= p^2).
    rewrite <- Heq; repeat rewrite fact_sq; 
    apply Zmult_le_compat; auto with zarith.
  omega.
assert (Hn2p: n < 2*p).
  elim (Zle_or_lt (2*p) n); auto; intros Habs'.
  assert (2*n^2 <= n^2).
    replace (2*n^2) with ((2*p)^2) by ring [Heq].
    repeat rewrite fact_sq; apply Zmult_le_compat; auto with zarith.
  omega.
assert (Hzwf : Zwf 0 (2*p-n) n) by (unfold Zwf; omega).
apply (IHn (2*p-n) Hzwf (n-p)); omega.
Qed.

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.