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

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

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.

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

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

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

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

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

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

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