Mathematicians talk of "proofs" as real things. But the only things that can actually happen in the real world are proof events, or provings, which are actual experiences, each occurring at a particular time and place, and involving particular people, who have particular skills as members of an appropriate mathematical community.
A proof event minimally involves a person having the relevant background and interest, and some mediating physical objects, such as spoken words, gestures, hand written formulae, 3D models, printed words, diagrams, or formulae (we exclude private, purely mental proof events, for reasons discussed below. None of these mediating signs can be a "proof" in itself, because it must be interpreted in order to come alive as a proof event; we will call them proof objects. Proof interpretation often requires constructing intermediate proof objects and/or clarifying or correcting existing proof objects. The minimal case of a single prover is perhaps the most common, but it is difficult to study, and moreover, groups of two or more provers discussing proofs are surprisingly common (surprising at least to those who are not familiar with the rich social life of mathematicians -- for example, there is research showing that mathematicians travel more than most other academics.)
The efficacy of some proof events depends on the components of a proof object being seen to be given in a certain temporal order, e.g., Euclidean geometric proofs, and commutative diagrams in algebra; in some cases, the order may not be easily infered from just the diagram. Therefore we must generalize from static proof objects to proof processes, such as diagrams being drawn, movies being shown, and Java applets being executed; hereafter, "proof events" and "provings" will have this meaning.
Mathematicians habitually and professionally reify, making it seem that what they call proofs are idealized Platonic "mathematical objects," like numbers, that cannot be found anywhere on this earth, but are nevertheless real. Let us agree to go along with this deception, and call any object or process a "proof" if it effectively mediates a proof event, not forgetting that an appropriate social context, an appropriate interpreter, and an appropriate interpretation are also needed. Then perhaps surprisingly, almost anything can be a proof! For example, 3 geese joining a group of 7 geese flying north is a proof that 7 + 3 = 10, to an appropriate observer.
A proof event can have many different outcomes. For a mathematician engaged in proving, the most satisfactory outcome is that all participants agree that "a proof has been given." Other possible outcomes are that most are more or less convinced, but want to see some further details; or they may agree that the result is probably true, but that there are significant gaps in the proof event; or they may agree the result is false; and of course, some participants may be lost or confused. In real provings, outcomes are not always just "true" or "false". Moreover, members of a group need not agree among themselves, in which case there may not be any definite socially negotiated "outcome" at all! Each proof event is unique, a particular negotiation within a particular group, with no guarantee of any particular outcome.
Going a little further, the traditional distinction between a proof giver and a proof observer is often artificial or problematic; for example, a group of mathematicians working collaboratively on a proof may argue among themselves about whether or not a given person has made substantive contributions. Hence we should use general terms like provers and proof participants, whatever their role and their distribution over space and time, and we should speak of "proof givers" and "proof observers" only to the extent that participants do so. (However, we will not consistently do this in practice, due to the resulting linguistic awkwardness.)
But practices and their communities are at least as important as proof objects and individual achievers; in particular, it is clear that these are indispensable for interpreting some experience as a proof; if you can't count, then you can't see geese as proofs, and if you don't know how to write and/or say the numerals "7", "3", "10", then you can't explain your proof to the decimal digit community. Of course, this line of thought takes us further from the objective certainties that mathematics often likes to claim, but if we look at the history of mathematics, it is clear that there have been many different communities of proving practice. For example, what we call "mathematical rigor" is a relatively very new viewpoint, and even within it, there are many schools, including various forms of formalism, intuitionism and constructivism. Moreover, the availability of calculators and computers is even now once again changing mathematical practice. For example, it is amusing to note that today, the most enthusiastic practitioners of logical formalism for mathematics are not logicians, let alone mathematicians, but rather computer scientists, who have built and who use many different computer-based systems to automate theorem proving, to a greater or lesser extent.
Mathematical logic focuses on small sets of simple, mechanical methods, called rules of inference, and explores claims that all proofs can be constructed as finite sequences of applications of such rules. While this approach is appropriate for foundational studies, and has been interesting and valuable in many ways, it is far from capturing the great diversity and vital living quality of natural proofs. In particular, it obviously entirely leaves out the social dimension of proofs, including their motivation and history.
Unfortunately, we lack the detailed studies that would reveal the full richness of mathematical practice, but it is already clear that proof participants bring a tremendous variety of resources to bear on proof processes. For example, a discussion among a group of mathematicians at a blackboard will typically involve the integration of writing, drawing, talking and gesturing in real time multimedia interaction. In at least some cases, this interaction has a high level "narrative" structure, in which sequentially organized proof parts are interleaved with evaluation and motivation (see Notes on Narrative for a deeper discussion of narrative structure).
Aristotle said "Drama is conflict", meaning that the dramatic interest, or excitement, of a play comes from conflict, that is, from obstacles and difficulties. Anyone who has done mathematics knows that many difficulties arise. But the way proofs are typically presented hides those difficulties, showing only the specialized bulldozers, grenades, torpedoes, etc. that were built to overcome them. Reading a conventional proof can be a highly alienating experience, because it is difficult or impossible to understand why these particular weapons were deployed. No wonder the public's typical response to mathematics is something like "I don't understand it. I can't do it. I don't like it." I believe that the mathematician's systematic elision of conflict is in large measure to blame for this. (Note also the military metaphor used above; it is surprisingly common in live mathematical discourse.)
So called "natural deduction" (due to Gentzen) is a proof structure with some advantages, but it is far from "natural" in the sense of being what provers do in natural settings; natural deduction presents proofs in a purely top down manner, so that, for example, lemmas cannot be proved before they are used. We need to move beyond the extreme poverty of the proof structures that are traditional in mathematical logic, by developing more flexible structures. But this is not enough. We also need more inclusive notions of proof that can accommodate more of the social context.
One simple step foward would be to allow alternative proofs that are incomplete, or even incorrect; this is an issue of structure, but it also requires attaching explanations to to proof parts. For example, to show why a lemma is needed, it is helpful to first show how the proof fails without it; or to show why transfinite induction is needed, it may help to show how ordinary induction fails. A history of attempts to build a proof records conflicts, and hence reintroduces drama, which can make proofs more interesting and less alienating. Of course, we should not go too far with this; no proof reader will want to see all the small errors a proof author makes, e.g., bad syntax, failure to check every hypothesis of a theorem before applying it, etc. As in a good movie, conflict introduction should be carefully structured and carefully timed, so that the clarity of the narrative line is not lost, but actually enhanced. Moreover, conflict is not the only element of context that may be helpful to proof readers; for example, concrete intuitions arising from applications, e.g. in physics, can be very useful.
The narrative structures of natural proofs seem to have much in common with cinema: there is a hierarchical structuring (of acts, scenes, shots in cinema, and of proof parts in mathematics); there are flashbacks and flashforwards; there is a rich use of multimedia; etc. The traditional formal languages for proofs are very improverished in the mechanisms they provide for structuring proofs into parts, and for explaining these structures and parts. We can learn much about how to improve proof structure by studying movies, because a movie must present a complex world, involving the parallel lives of many people, as a linear sequence of scenes, in a way that holds audience interest. We could also learn much about the role of motivation, conflict and emotion in holding the interest of viewers.
The Kumo system makes extensive use of the capabilities of recent web technology. Kumo generates a website, called a proofweb, for each proof attempt that it executes. This website has hot links to background tutorial material, including tutorial pages for each major proof method used, and for the novel mathematical theories used, such as hidden algebra. It also interleaves proof steps with explanatory material, according to conventions inspired by sociolinguistic analyses of narrative. In addition, it encourages provers to supply motivational material, such as interactive Java applets, and it uses a (precise version of) fuzzy logic that allows a smooth integration of informal proof parts with fully formal proof parts; this in particular allows an informal proof to be refined into a formal proof to whatever extent is desired.
No doubt there are many other exciting areas for further exploration in our quest to improve the understandability of proofs. Success on this quest could have a significant impact on mathematics education, given the impending pervasiveness of computers in schools, and the mounting frustration with current mathematical education practice. It could also make the current generation of more powerful theorem proving sytems accessible to wider groups of users and new applications.
The references below include not only further details on the Kumo system, but also some prior work by the author on the sociology of mathematics and information technology. A more formal version of the above material would of course include citations to relevant work in ethnomethdology and the sociology of mathematics, especially work of Harvey Sacks, Eric Livingston, and Donald MacKenzie.
The first reference below was written three years after (the first draft of) the present essay, and goes considerably deeper into certain issues that are only hinted at here, including the structure of natural proofs, and the value system of professional mathematicians.