What is a Proof?
by Joseph Goguen

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.)

The above deconstruction of "proofs" as objectively existing real things is only the first step in a more complex understanding. In addition to a proof object (or process), certain practices (also called methods) are needed to establish some experience as a proof event. For example, to interpret the flying geese as a proof about addition requires a practice of counting. This runs against the tendency, in mathematics, as well as in literature and linguistics, to insist on the "primacy of the text," ignoring the specific practices that are required to bring texts to life, and also ignoring the communities that embody those practices. It also runs against the tendency to celebrate the unusual achievements of particular "heroic" individuals.

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 above considerations motivate a novel notion of proof that is more inclusive and less purely formal than that of traditional mathematical logic, in that it involves not only formal proof methods and formal proof steps, but also involves motivation for the proof and its major steps, background information, and the large grain structure of the proof, including conflict and other narrative devices. This notion of proof, which draws on the sociological study of the actual practice of proving, has been implemented in the Kumo proof assistant and proof display system, which is described not only on its website, but also, in somewhat more detail, in the publications listed below.

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.

References

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.

1. Slides for The Reality of Mathematical Objects, lecture by Joseph Goguen for the UCSD Science Studies Colloquium, 20 November 2000; summarizes recent work applying discourse analysis, cognitive linguistics, ethnomethodology and semiotics to mathematical discourse and its natural ethics. There is also a pure postscript version. Warning: You may have to change the orientation of the pages from landscape to seascape; also, this is just a sketch of an unwritten paper, with many details missing.

2. Notes on Narrative. This is a brief overview of some techniques for the analysis of stories, including summaries of the structural theory of narrative, and techniques for the extraction of value systems from stories.

3. An evolving collection of proof displays generated by the latest Kumo proof assistant and website generator (version 4). This is part of the Tatami project, one goal of which is to make machine proofs much more readable than usual; the project has some emphasis on behavioral proofs for distributed concurrent systems.

4. Web-based Support for Cooperative Software Engineering, by Joseph Goguen and Kai Lin, in Annals of Software Engineering, volume 12, 2001, a special issue on multimedia software engineering edited by Jeffrey Tsai. An uncompressed postscript version is also available. This is an overview of the Tatami project and version 4 of the Kumo proof assistant and website generator, focusing on its design decisions, its use of multimedia web capabilities, and its integration of formal and informal methods for software development in a distributed cooperative environment. The paper is a revised and expanded version of the paper Web-based Multimedia Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin, which appeared in Proceedings, International Symposium on Multimedia Software Engineering, edited by Jeffrey Tsai and Po-Jen Chuang, IEEE Press, pages 25-32; this meeting was held in Taipai, Taiwan, December 2000.

5. Towards a Social, Ethical Theory of Information, in Social Science Research, Technical Systems and Cooperative Work, edited by Geoffrey Bowker, Les Gasser, Leigh Star and William Turner (Erlbaum, 1997) pages 27-56. A pdf version is also available. Presents a theory of information based on social interaction, and shows how values arise naturally in such a theory.

6. Brief text of keynote address Towards a Design Theory for Virtual Worlds: Algebraic Semiotics, with information visualization as a case study, by Joseph Goguen, given at the Virtual Worlds and Simulation Conference, Phoenix AZ, 10 January 2001. A sketch of algebraic semiotics and its applications, especially to scientific visualization and user interface design; the slides for the talk are also available. Warnings: Some figures shown in the lecture are not included; also, you may have to change the orientation of the slides from landscape to seascape. This talk is an update of the "distinguished" lecture Algebraic Semiotics and User Interface Design, given at the Institute for Software Research, University of Irvine, 20 October 2000, with some additional material on virtual worlds.

7. Are Agents an Answer or a Question? by Joseph Goguen. Position paper on agent technology, in Proceedings, JSAI-Synsophy International Workshop on Social Intelligence Design, 21-22 May 2001, Matsue, Japan. A pure postscript version is also available.

These notes were in part inspired by remarks of Eric Livingston, whom I wish to thank, though he is not to blame for any lapses from pure ethnomethodology that I may have committed. The remarks on narrative draw on detailed studies by the sociolinguists William Labov and Charlotte Linde.
To the Tatami project homepage.
To the CSE 271 homepage: User Interface Design: Social and Technical Issues.
To my homepage
Orignal version, 27 April 1997; edited November 1997 and March 1998, and then lightly re-edited in March 2000, and in July 2001, when the references were added.