Practical reasoning and the witnessably rigorous proof

Abstract

This paper introduces an anthropological approach to the foundations of mathematics. Traditionally, the philosophy of mathematics has focused on the nature and origins of mathematical truth. Mathematicians, however, treat mathematical arguments as determining mathematical truth: if an argument is found to describe a witnessably rigorous proof of a theorem, that theorem is considered—until the need for further examination arises—to be true. The anthropological question is how mathematicians, as a practical matter and as a matter of mathematical practice, make such determinations. This paper looks first at the ways that the logic of mathematical argumentation comes to be realized and substantiated by provers as their own immediate, situated accomplishment. The type of reasoning involved is quite different from deductive logic; once seen, it seems to be endemic to and pervasive throughout the work of human theorem proving. A number of other features of proving are also considered, including the production of notational coherence, the foregrounding of proof-specific proof-relevant detail, and the structuring of mathematical argumentation. Through this material, the paper shows the feasibility and promise of a real-world anthropology of disciplinary mathematical practice.

1 Introduction

By the late 1800s, an ever growing number of mathematical discoveries, technical problems, and methodological issues gave rise to debates among mathematicians concerning the practices of proving mathematical theorems (Kline 1972; Ewald 1996). This cauldron of activity influenced mathematics thereafter. It also led to the growth of the philosophy of mathematics as a distinct subdiscipline of philosophy, but one increasingly separated from the practical circumstances and problems faced by mathematicians. Over the course of the twentieth century, philosophers of mathematics predominantly came to view the foundations of mathematics as a problem concerning the nature and origins of mathematical truth (Beracerraf and Putnam 1964; Shapiro 2005; Irvine 2009).

From an anthropological point of view, perceived truths of the world are not matters of nature: they belong to the ways of a “tribe” and are generated and sustained by the real-worldly practices of its members. In the case of mathematics, the “tribe” of professional theorem provers, in practice, see written mathematical argumentation as the arbiter of mathematical truth: if the truth of a theorem is questioned, they examine the written argument that describes the claimed proof and try to establish the veracity of its reasoning. In this way, viewed anthropologically, the everyday production of witnessably rigorous mathematical proofs by, for, and among theorem provers might well be seen as the living, sustaining foundations of mathematical practice. The anthropological question is how provers go about producing and recognizing such proofs. This paper begins to develop an empirical, ethnographic approach to answering this question. In the case at hand, the paper examines the practical work that provers do to constitute and, therein, realize the reasoning of mathematical argumentation.

The immediate origins of this paper lay in attending to a familiar, recognizable feature of mathematical practice. By abuse of language, the written mathematical arguments that fill blackboards, textbooks, and journal articles are often referred to as “proofs.” The usage simplifies exposition, but such arguments are not proofs. They are descriptions of proofs or proof-accounts. Where, then, are the actual proofs of mathematical practice to be found? When provers seriously consider a proof-account, whether alone with pencil and paper in hand, in consultation with colleagues, or at the blackboard in the company of other provers, they engage in a process of working through the account, trying to find the reasoning and actions that the account describes and, therein, as a practically observable matter, establishing the adequacy or inadequacies of the account’s description. When successful, such pairings of accounts and the work of proving are discovered as coherent organizations of the practices of proving exhibiting the collegially witnessable, practically rigorous proofs of ordinary mathematical practice.

Section 3 is the heart of the paper. It considers, as an empirical matter, how the witnessability of such proofs is achieved. The section gives a detailed, ethnographic description of the process of working through a specific proof-account of a theorem of Euclidean geometry. Three features of this process are therein made plain. First, no matter how trivial and uninteresting some of this work may seem, the amount of practical work that is involved in working through the proof-account is massive. If provers did not do this work, they would not be able to find the proof that a proof-account describes. Second, provers give considerable effort to establishing the relevance of abstract, general explanations to the immediate proof-account: provers have to realize, and work to realize, the reasoning of a proposed proof in the specific details of that proof’s description. And, last, the reasoning involved in working through a proof-account is quite different from deductive inference as described in formal theories of mathematical argumentation. Native to the practical work of proving theorems, seemingly ignored in discussions of the nature and origins of mathematical truth, such reasoning is, to all appearances, pervasive in mathematicians’ work and unavoidable in situations of real-time proving. The paper argues that this reasoning is the handmaiden of deductive inference: it provides the glue that holds the argument together.

The final section of the paper places this material in the context of a developing anthropology of theorem proving. It sketches the origins and framework of the project, considers the relationship between often ignored aspects of proving and the witnessability of mathematical proofs, and shows the potential of such empirically oriented, anthropological studies. An “Appendix” to the paper briefly elaborates the pair structure of witnessably rigorous proofs.

2 The midsegment theorem

In Sect. 3, the proof-account in Fig. 1 will be used to examine the constitution of deductive reasoning. Nothing is particularly special about this proof-account. Our interests lie in the detail of things, not in abstract disputation: Fig. 1 provides a concrete example for our consideration. We want to see how deductive reasoning, rather than being an objective “thing”—transparent and self-exhibiting of its own truth—is an ongoing practical accomplishment.

Fig. 1

A proof-account for the midsegment theorem

Fig. 2

Theorems cited in the midsegment proof-account

Figure 1 is a description of a proof of The Midsegment Theorem, that the line segment between the midpoints of two sides of a triangle is parallel to, and half as long as, the third side. The proof-figure (the diagram in Fig. 1, a part of the proof-account) and the statements directly beneath the proof-figure restate the Midsegment Theorem in terms of what is to be understood as a general triangle $\triangle {ABC}$. For reference, the five theorems cited in the proof-account are collected in Fig. 2; all but one of them are part of the “natural” unfolding of the argument.

Theorem 1, “Pasch’s Axiom,” is different from the other cited theorems. The first step in Fig. 1 is to draw a line through the point E parallel to side ${\overline{AB}}$ of $\triangle {ABC}$. Nothing is wrong with this: drawing such a line is a standard straightedge and compass construction of elementary Euclidean geometry. Proposition I.31 of the Elements (Heath 1956) describes one such construction. The problem is whether the constructed line will intersect side ${\overline{BC}}$ of $\triangle {ABC}$. The proof-figure makes it look as if it does, but this is reasoning by diagram, not a deduction from the postulates of Euclidean geometry. Pasch’s Axiom, introduced by Moritz Pasch in the 1880s, assures us that such a point of intersection exists. More typical proof-accounts of the Midsegment Theorem (School Mathematics Study Group 1961, p. 267; Hemmerling 1964, p. 147; Jacobs 1974, p. 320; Lee 2013, p. 196) avoid the use of Pasch’s Axiom by giving an explicit construction of a specific point “F”.¹

The need to use Pasch’s Axiom (or to devise a constructive procedure that avoids it) is embedded in the cultivated skills of Euclidean geometry. Provers learn to attend to certain seemingly transparent features of a proof-figure—such as the place where two lines will meet—when no justification is given other than the visual appearance of the diagram.

A second technical remark concerns the measures of line segments and angles. In Fig. 1 and elsewhere, the congruence of line segments is treated as the same as the equality of their measures, and the two are used interchangeably without comment—that is, if two line segments are congruent, they have the same length and if two line segments have the same length, they are congruent. If the need arises, line segments are manipulated numerically in terms of their measures. Thus, we will write $k = {\overline{EC}}/{\overline{AC}}$ rather than using EC and AC without overlines for their associated numerical measures. Maintaining a distinction between geometric objects and their numerical measures would be a distraction and serve no immediate purpose.

Fig. 3

Two similar triangles

The heart of the proof is to show that the smaller triangle $\triangle {EFC}$ in Fig. 3 is similar to the larger one $\triangle {ABC}$. One way of doing this is to show that each of the pairs of corresponding angles is congruent. Since two angles of a triangle determine the third, only the congruence of two of the pairs of corresponding angles is needed (Theorem 3).

Let us suppose that $\triangle {EFC}$ is similar to $\triangle {ABC}$. This means that the two triangles have the same “shape,” that they are dilated or contracted versions of each other or, more precisely, that the ratios of the corresponding sides of the triangles are the same. Thus, if the two triangles are similar,

$$\begin{aligned} k = {\overline{EC}}/ \,{\overline{AC}} = {{\overline{EF}}}/ \, {{\overline{AB}}} = {{\overline{FC}}}/ \, {\overline{BC}} \end{aligned}$$

where the ratio k is called the constant of proportionality or the scale factor between the triangles. Since E is the midpoint of $\overline{AC}$, $\overline{AE} = \overline{EC}$. It then follows that $\overline{AC} = \overline{EC} + \overline{AE} = 2 \cdot \overline{EC}$, and the ratio of proportionality $\overline{EC} / \, \overline{AC}$ is $\frac{1}{2}$. This propotionality between all the corresponding sides of the triangles allows us to identify the congruencies between ${\overline{EF}}$ and ${\overline{DB}}$ and between ${\overline{FC}}$ and ${\overline{BF}}$ as marked in Fig. 4. What remains is to show that $\overline{DE}$ is parallel to ${\overline{BF}}$ (which is the same as being parallel to ${\overline{BC}}$) and that $\overline{DE}$ is congruent to ${\overline{BF}}$ which equals $\frac{1}{2} \, {\overline{BC}}$. Both these properties follow from the fact that DBFE is a parallelogram.

Fig. 4

Additional conguencies following from similarity

3 The constitution of deductive reason

Practical reasoning refers to the reasoning involved in organizing our immediate activities for the practical purposes of engaging in them. As one example, at some point when doing the vacuuming, we may find ourselves “vacuuming in rows”: pulling the vacuum back as we take a step to the side, then moving forward again to vacuum a new row slightly overlapping the previous one. By continually monitoring our actions, we keep our place in the vacuuming and try to insure that we’re covering the entire carpet. Or, as a second example, after taking the laundry out of the drier and dumping it on the bed, we enter into all the tasks of sorting and folding the clothes while, at the same time, organizing the bed space in order to facilitate the sorting and folding. Practical reasoning refers to the detailed, “microscopic” reasoning involved in such work for, as said previously, the practical purposes of doing it.

Initially, such reasoning may seem far from deductive logic and mathematical argumentation. To see the connection, we want to attend closely to the small details involved in working through the Midsegment Proof-Account. In particular, we will consider the actions and reasoning of maintaining the correspondence between the two-column display and the associated proof-figure, of establishing the relevance of propositional knowledge, and of realizing the organizational coherence of the described proof.

To begin, then, regarding the proof-figure in Fig. 1, we tend to think—both as a prospective undertaking and as a retrospective accomplishment—that a fixed, static correspondence exists between the proof-figure and the two-column display. In practice, the notational correspondence between the two is a continuing project used to visually identify features of the proof-figure. Statement 1 in the proof-account directs attention to ${\overline{EF}}$ as parallel to ${\overline{AB}}$. We look into the proof-figure to find the line segments to which reference is being made—that is, to see the placement of ${\overline{AB}}$ and ${\overline{EF}}$. We observe as well that ${\overline{AB}}$ and ${\overline{EF}}$ do appear to be parallel: the appearance of parallelism is a graphic reminder of their relationship in the proof.

The appropriateness of Pasch’s Axiom also needs to be worked out: A line through E parallel to ${\overline{AB}}$ intersects one side of $\triangle {ABC}$ at E. It cannot intersect ${\overline{AB}}$ because, by construction, the line is parallel to ${\overline{AB}}$. Nor can it intersect $\overline{AC}$ at the point C because, then, it would be identically the line $\overleftrightarrow {AC}$, and $\overleftrightarrow {AC}$ is not parallel to ${\overline{AB}}$. By Pasch’s Axiom (Theorem 1) it must intersect ${\overline{BC}}$ at some point in the interior of ${\overline{BC}}$. In the case of Fig. 1, that point has been called F. In working out this reasoning, we have spent considerable effort coming to understand how Pasch’s Axiom is being used: rather than Reason 1 transparently accounting for Statement 1, we have had to figure out, as a practical matter, how this could be so.

Finally, for some, the instruction in Statement 1 to “draw a line” and the justification “by construction” may not be familiar idioms. Independently of any historical or philosophical background, the practical import of the expression “by construction” is quite direct: it invites provers to recognize and acknowledge the legitimacy of using the auxiliary line through E in a proof-account of the Midsegment Theorem. In whatever way the line through E is introduced, the reason for doing so is entirely practical. The line segment ${\overline{EF}}$ is needed for this particular proof of the Midsegment Theorem: as an example, it is used immediately in Statements 2, 3, and 4 to exhibit the similarity of triangles $\triangle {EFC}$ and $\triangle {ABC}$.²

Turning now to Statement 2 in the proof-account, we see that it claims, by description, that $\angle {EFC}$ and $\angle {ABC}$ are congruent. When reading Statement 2, we visually trace the angles in the proof-figure. In the “Reasons” column, the description is justified by Theorem 2. One possibility is for us to find the specificity of Theorem 2 for the current situation of proving—namely, that $\overleftrightarrow {BC}$ is a “transversal” that “cuts” two parallel lines $\overleftrightarrow {AB}$ and $\overleftrightarrow {EF}$ (with the latter having just been constructed as parallel to $\overleftrightarrow {AB}$). Finding the specificity of Theorem 2 in terms of the immediate situation, we accept the claim that $\angle {EFC}$ and $\angle {ABC}$ are congruent.

Provers, of course, need not work or reason this way. The aim is not to legislate exactly what provers do or the precise details of their reasoning, but to bring to attention the type of miniscule, practical reasoning in which they are engaged. Provers may, for example, read the descriptive claim in Statement 2 (that $\angle {EFC}$ and $\angle {ABC}$ are congruent), look into the proof-figure, and see that $\overleftrightarrow {BC}$ crosses two parallel lines $\overleftrightarrow {AB}$ and $\overleftrightarrow {EF}$. Seeing this about $\overleftrightarrow {BC}$ might (or, depending on familiarity with Euclidean geometry, should) recall the property described in Theorem 2. Therein, in this way, provers may also come to substantiate the claim in Statement 2.

Although the “reasons” in the righthand column are supposed to be independent of, and justify, the associated descriptive claims in the proof-account (that is, the Statements), those reasons—as we have seen—actually feature in the process of confirming those claims. What the “reasons” mean in terms of the specific details of the proof-account and what their proof-relevant consequences are, are themselves accomplishments of practical reasoning.

For Statement 3 that $\angle {ECF}$ is congruent to $\angle {ACB}$, we, again, visually trace the two angles $\angle {ECF}$ and $\angle {ACB}$ in the proof-figure; we see that their descriptions (that is, their descriptions as “$\angle {ECF}$” and “$\angle {ACB}$”) describe one and the same angle. This is the practical sense we make of Reason 3. At the same time, a slightly larger question can arise: what is the point in working through these statements? The question is not critical at this point; it is more a matter of getting a sense as to where the proof is going. Step 4 clarifies the situation: the observations in Statements 2 and 3 have been put together to lead to, and as the immediate grounds for, the description of $\triangle {EFC}$ and $\triangle {ABC}$ as similar triangles. Part of reading the first three steps of the proof involves looking for the organizational coherence of the proof that gives intention to the way that the statements of the proof-account have been ordered. Statement 4 provides the grounds for understanding that intention or, said differently, for following the developing orderliness of the proof.

Up to now, what ties this reasoning together is the retrospective-prospective character of a prover’s ongoing inquiry into the organization of the proof-account. Provers retrospectively come to understand why they have been doing what they have done, and they look forward to the rest of the proof to figure out what their work will come to. None of this is explicit in the proof-account except in the way provers are looking for and finding this intentionality, again as their own achievement, in the organization of a proof-account’s statements.

The critical claim is Statement 5 and the identification of 1/2 as the scale factor. Once again, the stated reason places the burden on the reader to find what is being claimed and to see how the calculation of the scale factor can be made. Looking at the proof-figure, one sees that E is the midpoint of $\overline{AC}$ and, therein, finds that the ratio of two of the triangles’ corresponding sides: $\overline{EC}/\overline{AC} = 1/2$. To stress the point, this is the practical reasoning of finding the organization of practices that the proof-account describes. It is also the “easy part.” The reader must understand what is being proposed about $\triangle {EFC}$ and $\triangle {ABC}$, what the “constant of proportionality” is, and how this constant features in the developing proof.

Statements 6 and 7 follow from the similarity of $\triangle {EFC}$ and $\triangle {ABC}$, but how they follow is again left to the reader. As “trivial” or as “obvious” as such matters may seem, provers nevertheless have to work them out. The two statements are clumped together in that they both follow directly from Statement 5. Statement 6 leads to seeing and working out that ${\overline{FC}} = {\overline{BF}}$: from the proportionality between the sides of similar triangles, ${\overline{FC}}$ is 1/2 ${\overline{BC}}$, and if ${\overline{BF}}$ is 1/2 ${\overline{BC}}$, then ${\overline{BF}} = {\overline{FC}}$. (Variations on this reasoning are possible; the point is that provers engage in reasoning that substantiates the claim in Statement 6.)

Although provers must wait to find the relevance of Statement 6 (and provers recognize this as they move to Statements 7 and 8), the relevance of Statement 7 is immediate. Statement 7 asserts that ${\overline{DB}} = {\overline{EF}}$ for which readers need, in some way, to justify the claimed equation ${\overline{DB}} = \frac{1}{2} {\overline{AB}} = {\overline{EF}}$. Following this, the reference to Theorem 4 in Reason 8 draws attention to the fact that the parallelism and congruence of ${\overline{DB}}$ and ${\overline{EF}}$ have already been established. This parallelism and congruence establish the relevance and applicability of Theorem 4 (that DBFE is a parallelogram), further clarifying the organization of the developing argument.

The rest of the argument can be understood in terms of what the described proof is supposed to demonstrate. One of the aims is to show that $\overline{DE} = {\overline{BF}}$; the other is to show that $\overline{DE} = \frac{1}{2} {\overline{BC}}$. Visually, by looking at the proof-figure (and as established in Statement 8), $\overline{DE}$ and ${\overline{BF}}$ are opposite sides of a parallelogram. A property of parallelograms (Theorem 5) is that opposite sides are congruent. (If we need to prove this, the proof is both simple and clever: one of the diagonals of a parallelogram is drawn in a proof-figure; the congruence of the two resulting triangles is established because the diagonal is a transversal, first to one pair of opposing sides and, then, to the other pair.) The difficulty in Statements 10 through 11 for the writer of the proof-account is figuring out how to arrange the numerical calculations so that they seem transparent; for the reader, the problem is to work through the proof-figure to see what is being calculated and to realize why this is being done. Statements 10 through 11 bring closure to the proof by claiming/describing those features of the proof-figure that the restatement of the Midsegment Theorem in Fig. 1 asserts to be true.

That the last statement and last reason are the last statement and reason is understood to signal that the argument has been completed and that what has been said is sufficient to exhibit the proof of the theorem that has been claimed. If this is unclear, provers need to consider that the argument has concluded and find how this could be the case. Such claims are often marked syntactically using “Q.E.D.”, the Halmos symbol “$\square$”, or a similar device.

To many, all this will be seen as focusing on trivial matters and belaboring the obvious. That is, of course, what we have done and what we are interested in. Practical action and reasoning are not “the stuff as [mathematical] dreams are made on.” Except, in a peculiar way, maybe they are. By describing these actions and reasoning in detail, we are not saying that provers consider them, beyond the immediate moment, as important or as achievements. They are achievements-in-the-small. Provers tend to devalue what they have been doing in light of practical reasoning’s local and global accomplishments—locally, finding the clarity and continuity of the assertions of the textual proof-account; globally, realizing the organizational coherence of the projected proof as an exhibition of the truth of the Midsegment Theorem.

Because provers come to trivialize and forget the practical work that they have done in working through a proof-account, the arts of practical action and reasoning come to appear as anything but essential to finding witnessably rigorous proofs. Yet, in real time, provers cannot work through a proof-account without engaging those skills nor, when the details of such accounts are questioned, can provers undertake a review of the account without animating it with the practical arts of proving that the account implicitly attempts to describe. All the apparently forgettable, obvious, trivial practical actions and reasoning of working through a proof-account are the actions and reasoning that provers do, and must do, to find, recognize, and witness a proof of the Midsegment Theorem.

4 An anthropology of proving

This paper is part of a developing anthropology of professional, disciplinary mathematical theorem proving. Two observations were essential to the project’s inception: one involved the fundamenta viva of proving, the other, the nature of mathematical practice. The relevance of these observations as well as the need for an anthropology of proving are both, in an odd way, anticipated in contemporary philosophy.

Philosophers have predominantly viewed the foundations of mathematics as an abstract, theoretical problem and as a problem concerning the nature and origins of mathematical truth. Recently, philosophers of mathematical practice have challenged this traditional conception (see, for example, Mancosu 2008). Although not completely clear on the matter, the new studies suggest, at least implicitly, that continued work on the traditionally-conceived problem of philosophical foundations is somewhat confining, insular, and unpromising (Mancosu 2008, p. 5). The proffered solution has been a turn to “mathematical practice” and the development of philosophies of features of contemporary mathematics—as a hypothetical example, the development of a philosophy of structural reasoning in higher-dimensional algebraic topology. There are few indications of what might be meant by “mathematical practice” (Carter 2019) and, despite the fact that papers in this new field are sometimes filled with highly technical, advanced mathematics, few if any attempts are made to apply such philosophies to the situated doings and practical concerns of provers trying to prove theorems.

Like the philosophy of mathematical practice, an anthropology of proving also involves a turn away from the abstract, theoretical concerns of traditional philosophical studies of the foundations of mathematics; it involves a turn to the study of mathematical practice as well. The direction of the research, however, has been different. A first and fundamental observation of the anthropological studies was that professional mathematicians, as a practical matter and as a matter of practice, treat written mathematical argumentation as the arbiter of mathematical truth: theorem provers write and work through textual arguments to exhibit or substantiate the claimed proofs that the arguments are inteneded to describe. Without this production, evaluation, substantiation, and recognition of practically rigorous proofs by, for, and among mathematicians, there would be nothing about which philosophers of mathematics could inquire. From an anthropological point of view, it seemed and still seems reasonable to attend to the ways that theorem provers make proofs witnessable to and for each other. These ways of proving can be seen as the living substance of mathematical truth and, therein, make mathematical truth into a matter for empirical, anthropological, and social investigation.

Regarding the study of mathematical practice, a second observation also lies at the origins of an anthropology of proving. Put simply, when engaged in proving theorems, theorem provers are engaged in and literally do work. Some of the work of elementary Euclidean geometry was described in Sect 3. All provers know this work—they have to know it in order to produce practically witnessable proofs. Few want to talk about its practical, ordinary, and sometimes messy, even embarrassing details. Nevertheless, it is just this work that makes references to “mathematical practice” definite and concrete. This is not to deny insight, creativity, experience, and whatever else: acknowledging mathematical practice as the practical, recognizable work of proving emphasizes the things about which provers have insight, are creative, anticipate and fashion new lines of inquiry, find hitherto ignored or misunderstood connections. They are the practices that provide the background against which proofs are discovered as organizations of those same practices. A few examples involving the cultivated skills of professional disciplinary mathematics will help make the substance and intention of the proposal clear.

Finally, along with these two observations, a research directive began to develop to help guide ongoing and future research. As an example, the following discussion briefly considers the encultured and continually monitored skills involved in producing coherent notation, in maintaining an appropriate level of proof-relevant detail, and in arranging and exhibiting the witnessable structure of a mathematical argument.³ Rather than treating these skills as distinct competencies, the research directive is to examine how the particulars of such skills, in and as the details of their use, are bound together as the work of producing and exhibiting witnessably rigorous proofs.

Consider, first, some of the details surrounding the production of coherent notation. Statement 2 in Fig. 1 claims that $\angle {EFC}$ is congruent to $\angle {ABC}$. What if, instead, Statement 2 read “$\angle {CFE}$ is congruent to $\angle {ABC}$.” In one sense, nothing is wrong: $\angle {CFE}$ identifies the same angle as $\angle {EFC}$, at least for the purposes of the present proof-account. Nonetheless, although a minor detail, provers immediately recognize that something is wrong: they are being asked to identify angles by visually tracing them in opposite directions. An additional “step” has been interposed between Statement 2 and literally seeing what it proposes. Similarly, Statement 6 (${\overline{FC}} = \frac{1}{2} \, {\overline{BC}} = {\overline{BF}}$) and Statement 7 (${\overline{DB}} = \frac{1}{2} \, {\overline{AB}} = {\overline{EF}}$) trace the line segments in the same direction. While there is nothing substantively wrong if the directionality of the segments were mixed up—e.g., ${\overline{FC}} = \frac{1}{2} \, {\overline{CB}} = {\overline{BF}}$ and ${\overline{DB}} = \frac{1}{2} \, {\overline{BA}} = {\overline{FE}}$—these changes make provers do extra work in order to find what is being claimed in and through the proof-figure.

In terms of the foundations of mathematics, such details may seem insignificant except that the more such notational “infelicities” are present, the more difficult it is to find the proof that a prover is trying to describe. In a completely unanticipated way, the encultured skills of writing coherent notation are part of the living, real-time foundations of mathematical truth.

The same is true regarding the skills of maintaining an appropriate level of proof-relevant detail. A few examples should give the idea. First, in discussing Reason 1, the text of Sect. 3 and an associated footnote offered a somewhat extended treatment of the expression “by construction.” For the practical purposes of working through the proof-account, the digression was and is without point. Given the context, provers either understand the point of the explanation or they do not. In a different way, the explication of the application of Pasch’s Axiom in Sect. 3 does not belong in the proof-account either. At the level of proving the Midsegment Theorem, the use of Pasch’s Axiom is a technical consideration: mentioning the axiom is required by current standards of rigor; the explication of its relevance and use through added statements and reasons in the proof-account would distract attention from the witnessable proof that is being described. The elaboration of the axiom’s use is left to the reader. The same is true of the other named theorems listed in Fig. 2. If elaborated, the proof-account would be buried in a mass of technical and subsidiary details. Viewed from the standpoint of producing a witnessably rigorous proof, the skills of foregrounding and backgrounding mathematical details are crucial.

Last, and again only briefly, the skills of arranging and exhibiting the witnessable structure of a mathematical argument should be considered. This was already stressed in Sect. 3 and is tied to the production of coherent notation and the work of foregrounding proof-relevant details. The focus here is on what may also appear to be a small and unimportant detail.

Figure 5 presents a part of the proof-account of the Midsegment Theorem. Central to the projected proof, lines 2 through 4 argue that $\triangle {EFC}$ is similar to $\triangle {ABC}$. The manner in which the lines are written appears so natural that it is difficult to see any intelligence behind them. In textbooks on grammar and composition, the structure is called “parallel construction.” Following the notational conventions for describing features of the triangles, the left side of the “ledger” in Statements 2 and 3 identifies features of $\triangle {EFC}$ which are compared with features of $\triangle {ABC}$ appearing on the right. Statement 4 then makes the point of the preceding lines with $\triangle {EFC}$ again appearing on the left and $\triangle {ABC}$ appearing on the right. If the positions of the angles in Statement 3 were exchanged (for example, “$\angle {ACB}$ is congruent to $\angle {ECF}$”), a prover has to work out that the intended order is the one given in Statement 3. If, as well, $\angle {ECF}$ were written as $\angle {FCE}$, reading the proof-account would become increasingly problematic.

Fig. 5

The use of parallel structure

As a matter of common experience and recognition, as the visible presence of these skills decreases, proof-accounts become increasingly difficult to read and their intended proofs increasingly difficult to understand. Provers live in a world of technical and detailed practices; many if not all these practices, particularly in the specifics of actual proving, are tied to the exhibition of witnessably rigorous proofs. Such observations give support to the possibility of a fundamenta viva of proving: in the day-to-day circumstances of ordinary theorem proving, mathematics does not rest on transcendental truths but on the cultivated practices of professional, disciplinary mathematics. The examples illustrate as well the directive to see how these skills fit together as the work of producing and exhibiting witnessably rigorous proofs.

Regarding the central argument of this paper, an apparently widespread belief is that application of deductive logic guarantees the the truth of mathematical inference or, more formally, the truth-preservation of mathematical argumentation. This paper does not argue that this conception of rigorous argumentation and mathematical truth is wrong; neither does it argue that it is right. It argues, instead, that deductive reasoning does not stand alone. When working through a proof-account, provers are actively engaged in establishing, or constituting, the deductive logic that the proof-account is supposed and, retrospectively, is seen to describe. The same inextricable reliance on practical reasoning holds for discovery work: proof-accounts are the interface between provers; a proof-account attempts to shape the skills of proving to make witnessable the logic of a discovered proof.

The problem as well as the promise of an anthropology of proving is that it offers no external, Archimedean position from which to view provers’ work. For provers working through proof-accounts, they are engaged in all the practical actions and reasoning of finding, realizing, and making witnessable the proofs that are being described. From within that work, the deductive structure of that work is their ongoing achievement. To ask what the relationship is between a proof’s deductive structure and the messy practical work of real-time proving, the answer is that it is what it observably is seen to be, the practical, situated, real-time work of finding, realizing, and making witnessable that structure. The same is true for discovery work. If provers engaged in discovery work were asked to describe the logic and structure of their prospective discoveries, they would have to ask their interlocutors to wait until they discovered the witnessable proofs that they were trying to find. If, on the other hand, they were asked to describe the logic and structure of their immediate work, they could offer all the messy details, practical reasoning, and anticipated possibilities of what they were presently doing and trying to do.

Overall, the aim of this paper has been to show the cogency and feasibilty of an anthropology of proving and, more specifically, the feasibility of studying mathematical truth in and as the day-to-day circumstances of ordinary theorem proving. The idea of an anthropology of proving is to hold a microscope on the work practices of professional theorem provers and attend to the details of what they are observably doing, both alone and together, as practicing mathematicians. Once we turn away from the abstractions of the foundational problem and begin to look at the real-time, situated, detailed work of proving theorems—by provers alone and working together—a world of unanticipated phenomena opens for empirical investigation.

Appendix: The witnessably rigorous proof

A fuller discussion in the body of this paper of the collegially witnessable, witnessably rigorous proofs of ordinary mathematical practice would have distracted attention from the paper’s more immediate aims. Such proofs are the pairing of descriptions of proofs (proof-accounts) with the lived, practical work of proving that such descriptions depend upon and implicitly describe. The pairing of the proof-account in Fig. 1 of Sect. 2 with the practical actions and reasoning described in Sect. 3 provides one example.

As a second example, consider a standard proof-account of the uniqueness of the identity element of a group. One supposes that there are two such identity elements, e and $e'$. Then $e'= e *e' = e.$ QED. Essential to seeing and realizing the witnessably rigorous proof, provers need to read the expression $e *e'$ in two ways—as the element $e'$ multiplied on the left by the identity e and as the element e multiplied on the right by the identify element $e'$. If it made pedagogical sense to add such a statement to the proof-account, provers would still have to engage in the physical actions of reading $e *e'$ in both ways to find the proof that the proof-account prospectively describes.

Fig. 6

The diagonals of a rhombus are perpendicular and bisect each other

Another example is provided by a proof-account that the diagonals of a rhombus are perpendicular and bisect each other. A brief proof-account including Fig. 6 might read: “Each of the diagonals lies on the perpendicular bisector of the other. QED.” The witnessably rigorous proof depends on actually (literally, with the eyes) seeing that the diagonals are perpendicular bisectors. The proof-account, including the proof-figure, are just text- and drawing-on-the-page: they do not prove anything. The joining of the account with the physical perception of the diagonals as perpendicular bisectors is an essential part of the observable proof.

These two examples—the uniqueness of the identity element and the property of the diagonals of a rhombus—show the occasional, dramatic starkness of such pairings and their centrality to a proof. Sect. 3 of the text illustrates the omnipresence and ordinariness of the pairing of proof-account and the work of proving throughout the proof of the Midsegment Theorem.

Fig. 7

A Proof-in-the-Diagram Puzzle (Jenks 1949, p. 73)

Another way of coming to see and appreciate the pair structure of proofs is afforded by the “Find-the-Proof-in-the-Diagram” exercises of elementary geometry textbooks. These exercises pose two problems. No proof “lives” in a diagram: the first problem is to visually find how the features of the diagram are germane to the work of proving the claimed theorem. In the case of Fig. 7, a key realization involves the theorem that the measure of an inscribed angle is equal to half the measure of its intercepted arc. The second problem is to write a proof-account that describes the envisioned proof in terms of specific diagrammatic detail. For Fig. 7, the theorem that congruent chords in congruent circles cut off congruent arcs may be relevant and, therein, so to the need to introduce additional notation into the diagram.

As in Fig. 7, find-the-proof-in-the-diagram exercises often illustrate, in an immediate, visual way, that proof-accounts can lie at a distance from the initial perception of a prospective proof. The exercises help teach the practical arts of writing proof-accounts and how the unexplicated practical skills of proving can be articulated by them.