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.