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

Solution 1:

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.

Solution 2:

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.

Solution 3:

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.

Solution 4:

Why? Because this has been the most efficient way to communicate proofs, as shown by the answers of Brian M Scott and Pew.

But that may not always be so.

Mathematical theorems in journals now often reach tens or hundreds of pages, for example, the famous proof of Wiles's Theorem, or the Classification of All Finite Simple Groups (itself an ongoing project with key theorems still being coded into proof checkers). As knowledge expands, two things happen: either new fields (of subject matter, not the commutative ring with invertible multiplication) are explored, or the complexity of "technologies" increases. A proof often now reaches the complexity of a medium sized class library; something akin to tens of thousands of lines of high level computer code. In the early days of high level language programming, individual programmers cut and tested their own codes, which, once "proven" (by enough testing) were seldom disected again by other people, whom such codes were often incomprehensible to. Procedures and paradigms evolved to handle more and more software complexity: structured programming championed by such workers as Niklaus Wirth; later object oriented programming and various management theories for software quality control. A well documented piece of code is very like a natural language mathematical proof in many ways: its comments, design and structure should show the reader exactly how it does what it claims to do and the actual high level statements themselves provide the recipe to be encoded by the compiler.

The complexity that can be handled in these new paradigms is astounding: whereas the development of Fortran under the leadership of John Backus (of the Backhus-Naur metalanguage fame) took 18 staff years, computer science students now write their own compiler as late undergraduate or early undergraduate exercises and, with a bit of reading, the principles of compiler working are readily understood by almost anyone with training (see, for example, Appel, Andrew W. (1998),“Modern Compiler Implementation in C”, Cambridge University Press, New York, Cambridge. ISBN 0-521-58390-X. See esp. Chapter 2.).

Likewise Mathematics has evolved its own complexity handling paradigms. Two great examples of this are Noether's notion of Begriffliche Mathematik, which drove much of the modern approach abstract algebraic structures and category theory, although a logical, mathematical language in itself, also plays this role of giving a very large scale, top-down view of a mathematical problem: it bears a great deal of likeness to several software modelling metalanguages insofar that the latter are aimed at identifying and studying morphisms between objects within categories: in software design more often described as the something like the formal definition of "use-cases" or "processes" comprising "collaboration" between "actors" or "agents". The language of category theory is even heavily borrowed in software design and architecture.

But it may be that natural language in mathematics, or, equivalently, high-level languages and modelling languages in software design is reaching the limits of its capability. Fascinatingly, formal proof checkers are now finding their way into the proving of critical software systems. For example:

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish1, Thomas Sewell, Harvey Tuch, Simon Winwood, "seL4: Formal Verication of an OS Kernel" in In 22nd ACM Symposium on Operating Systems Principles (SOSP) (2009)

describes in detail the proof of the correctness of implementation (i.e. the equality of the software's behaviour with a formal specification) in the theorem prover Isabelle. One thing is for sure: formal theorem provers will become more and more important as softare systems, and mathematical proofs, rise above the complexity that can be handled by one human being. One of the comments also alludes to other like projects:

...on the other hand if we want very high assurance of correctness we need to use machine-verifiable proofs in programming as well. For example the entire Windows Hyper-V hypervisor has been verified to be free of certain kinds of errors because it is such a security-critical component. (User usr)

Just to close: using a software theorem prover to "prove" the soundness of software may seem like question begging, but it isn't really. The core of the theorem prover is simply a parser which tests the conformance of the proof steps with formal definitions of the rules of inference. If you read the Appel reference "Modern Compiler Implementation" I cited above, you can come to understand that a parser is actually a very simple program taking up at most a few pages of high level code and whose working has been thoroughly described in high level language and thoroughly understood by thousands of reviewers. Of course, something like Isabelle is much more than this, but it doesn't matter if there are bugs in the proof construction tools in Isabelle: as long as a constructed proof is sound (complies with the correct rules of inference), it will pass the proof checker. If a bug arose in the proof construction tools that led to an incorrect proof, it would be picked up in the last checking phase.