2.1. The role of proofs in mathematical practice

The notion of mathematical proof plays a central role in mathematical practice.Footnote ² ‘Proof’ is a success term, indicating that a sufficient level of epistemic support for a theorem has been reached for the result to be relied upon. Proof is a binary notion: a theorem has either been proven or it hasn't, and a theorem which approximates proof does not enjoy the same privileged position. A proof can be better or worse – more beautiful, simpler, more useful, clearer, more explanatory – but these dimensions of gradability refer to the aesthetic qualities of a proof and its mathematical virtues rather than the strength of its epistemic position. Proof is an inquiry stopper: once a theorem has been proved, you can't make it more proven, and so the interest in reproving established results lies in developing new techniques or ideas, or increasing the higher-level confidence that the proof didn't contain an error, as discussed by Rav (Reference Rav1999), Avigad (Reference Avigad2006), and Dawson (Reference Dawson2006). A theorem with a proof is actionable: the theorem can be properly asserted in conversation, and it can be properly cited and relied upon in the proofs of other theorems. As epistemologists would say, there appears to be a proof norm of assertion and citation in mathematics (Weiner Reference Weiner2007).

Proofs serve multiple functions in mathematical practice. First of all, they solidify mathematical ideas, filtering the messy everyday process of mathematical inquiry into a concrete piece of reasoning. The standards of mathematical writing force a certain degree of clarity and precision, creating fairly rigorous standards for a piece of reasoning to count as a proof. Secondly, a proof serves as a vehicle for communicating reasoning to other mathematicians. A proof can be written down, presented, emailed around the world, and published in a journal. Thirdly, a written proof serves as a permanent record of a piece of reasoning, something which can be checked, consulted, and passed on to future generations.

There is a close analogy between the role of proof in mathematics and the role of discovery in empirical science.Footnote ³ Empirical discoveries are important to our stories about progress in science, marking the moment when ignorance becomes knowledge, and when a claim enters the realm of scientific knowledge. Discovery is also central to the scientific inquiry because it is a private (i.e. rivalrous and excludable) good that can form the basis for an incentive structure that motivates scientists, leading to them working harder and dividing up their efforts across different problems and methodologies (Merton Reference Merton1957; Zollman Reference Zollman2018). The priority rule for publications is written into scientific history by discoveries which are named after their discoverer(s) (35P/Herschel–Rigollet, the Mpemba effect, the Quassi plant genus, and the Apgar score).

Similarly, proof marks the moment when ignorance is resolved, and a theorem becomes part of the mathematical community's knowledge. It is also central to the stories we tell about mathematical progress (brought out, for example, in the Jaffe–Quinn debate (Jaffe and Quinn Reference Jaffe and Quinn1993; Atiyah et al. Reference Atiyah, Borel, Chaitin, Friedan, Glimm, Gray, Hirsch, Mac Lane, Mandelbrot, Ruelle, Schwarz, Uhlenbeck, Thom, Witten and Zeeman1994; Thurston Reference Thurston1994)). Proof is also closely connected to the publication economy in mathematics. Mathematics ostensibly operates with a priority rule for proof with some flexibility for contemporaneous proofs, and for later improvements and refinements. Typically important theorems are named after the people that proved them (Noether's theorem, Cauchy–Kovalevskaya theorem, Rao-Blackwell theorem).Footnote ⁴ In both cases these naming practices and the histories told around them tend to skew our understanding of inquiry towards individualism, creating a tendency to see all intellectual progress as individual efforts.

2.2. Proofs and mathematical knowledge

Although mathematical knowledge is distinctive in a number of ways, it shares a basic structure with other kinds of knowledge. We will assume that knowledge in general involves correct belief that is based on epistemic support, with no undefeated defeaters. This gives us the following conditions on having mathematical knowledge of some theorem p:

We won't have much to say about mathematical correctness: what one thinks about it will depend on background views about mathematical ontology.

We assume that mathematical knowledge requires believing that the mathematical proposition is correct, being disposed to employ it in suitable proofs, and to assert it in relevant conversation. Group mathematical knowledge will similarly require a kind of doxastic commitment on the part of the knowing group. This commitment might be understood in terms of consensus or joint commitment to some proposition (Gilbert Reference Gilbert1987) or in terms of dispositions to assert, use as a premise, or in the mathematical case cite as a theorem (Habgood-Coote Reference Habgood-Coote2019a, Reference Habgood-Coote2020).

With non-mathematical knowledge, epistemic support often comes in the form of evidence provided by other propositions the agent believes. Although mathematical knowledge can be based on evidence (we can have mathematical knowledge via testimony, through probabilistic reasoning, or by relying on a mechanical or electronic computers), it is unclear to us whether (and how) performing a proof could count as evidence for a theorem. We understand knowledge based in proving activity as a kind of non-evidential knowledge, in which epistemic support is produced by proving activity. There is an attractive model for this kind of knowledge in the form of virtue-theoretic analyses of knowledge, which understands knowledge as true belief due to an act of intellectual virtue (Zagzebski Reference Zagzebski1996; Sosa Reference Sosa2007), and we will similarly understand knowledge based in proving activity as a true mathematical belief that is due to properly executed proving activity (Tanswell Reference Tanswell, Brown and BeunoForthcoming).Footnote ⁵

Mere epistemic support is not sufficient for mathematical knowledge. Say Zayn carries out a piece of long division, performing the calculation correctly, and reaching the right result. They still might fail to know the answer to the sum. They might receive rebutting evidence from a peer who reached a different result. Or they might get undercutting evidence, in the form of a (misleading) evidence that they are working under the effects of a drug that interferes with calculations. We will assume that both rebutting and undercutting evidence can function as knowledge-removing defeaters.

With this background in place, we can distinguish a number of different kinds of knowledge associated with mathematical proofs.

One kind of knowledge is knowing that a theorem is correct. This bare propositional knowledge is neutral on support, and might be based on having proved the theorem, on someone else having proved the theorem and testified to its truth, or perhaps on probabilistic or computational methods. Propositional knowledge of a theorem is mathematical knowledge in the sense that it has a distinctive object, but it need not involve a distinctive kind of epistemic support or inquisitive activity.Footnote ⁶

Turning to talk about ‘knowing a proof’, we can distinguish two kinds of knowledge: objectual knowledge of the proof, and what we might call knowledge from proving activity.

Objectual knowledge is the kind of knowledge that we refer to when we say that someone knows a person, a place, or a coding language. It involves both understanding the object, and some knowledge-how. Objectual knowledge of the proof of Fermat's last theorem involves understanding the shape of the proof, its key steps, and knowing how to carry most or all of them out. The know-how involved in understanding a proof will often be partly tacit knowledge which is not expressible in language, but rather in working out how to solve mathematical problems (Habgood-Coote Reference Habgood-Coote2019b). This kind of knowledge does not require actually having carried the proof out: the students in a class who have just watched an instructor prove the Pythagorean theorem know that proof, in the sense that they understand it, and know how to carry it out by themselves. Objectual knowledge ascriptions are gradable – we can know a proof better than you do – and the standards required for knowing a proof can differ depending on the context. What is required from primary school children to know a proof of the Pythagorean theorem will be different to what is required from first-year university students.

Knowledge from proving activity is the kind of knowledge that we distinguished above, whereby having correctly and rigorously performed the proof provides the support for the belief that the theorem is correct. This kind of knowledge requires having carried out a proof, and believing the theorem on that basis. Knowledge from proving activity involves propositional knowledge of the theorem, correct proving activity that manifests knowledge how, and understanding of the theorem. However, the carrying out or performing a proof doesn't mean that one has to invent the proof. One can also gain knowledge from proving activity by reading through a proof and carrying out and following the reasoning it describes.

2.3. From individual to social features of proofs

We claim that the standard conception of proof is individualistic, because a proof is understood as a device for communicating knowledge between individuals, and because the criteria for a successful proof are defined in individualistic terms.Footnote ⁷

On the standard conception a proof is an interpersonal communication device: one person gains knowledge from proving activity, then can pass it to another, who may read the proof and then also gains objectual knowledge of the proof or knowledge from proving. Although this transaction takes place between individuals it has a limited role for wider social factors.

To bring out the second sense in which the traditional conception of proof is individualistic, let us consider some properties which are supposed to be necessary for proof: surveyability, transferability, and convertibility. The first comes from Tymoczko's discussion of the Four Colour Theorem (Reference Tymoczko1979)Footnote ⁸ and the latter two from Easwaran's (Reference Easwaran2009, Reference Easwaran2015) discussion of probabilistic proofs. We are not committing to these as necessary or sufficient conditions of proof, but instead take them to capture some of the thinking that has been exhibited in the literature on how the mathematician features in properties of proofs. These features are also importantly related to our later discussion. Let us take these in turn.

Firstly, Tymoczko argues that proofs must be surveyable:Footnote ⁹

To be surveyable means that the proof can be understood and checked as a complete whole, where each individual step is a step toward the aim of establishing the theorem. Surveyability in the sense used here is individualistic property, involving a single agent comprehending the proof in full. Tymoczko is also linking this comprehension to the individual agent's mathematical knowledge gained from the proof, as we described above.Footnote ¹⁰ The notion of surveyability has developed further in the literature, such as in Azzouni (Reference Azzouni1994: 166–71), Bassler (Reference Bassler2006) and Coleman (Reference Coleman2009), including some tentative thoughts from Azzouni that we need to consider the group level of the mathematical community (Azzouni Reference Azzouni1994: 166–71).

Secondly, let us consider transferability, as discussed by Easwaran (Reference Easwaran2009):

For Easwaran transferability is a social epistemic virtue pertaining to the importance of proofs as communicative devices. The benefit of a transferable proof is that an individual mathematician reading it does not need anything further from the author of the proof: they can decide the merits of the proof entirely based on what is presented to them. Easwaran argues (Reference Easwaran2009: 356) that this is also an important property for proofs to have to enable the mathematical community to monitor and check the established literature. Furthermore, Easwaran points to the potential problem of long or exceptionally complicated proofs being beyond the reach of any individual mathematician. Nonetheless, for our purposes there is still an individualistic essence to transferability. A successful proof puts a reader in a position to know the theorem just by exercising her own mathematical reasoning, removing the need for reliance on testimony and authority. Indeed, the “relevant expert” is in the singular here, since multiple experts working together would potentially introduce testimonial evidence back into proofs, something Easwaran is precisely looking to avoid.

Thirdly, Easwaran (Reference Easwaran2015) builds on the work of Lakatos (Reference Lakatos1976) to argue that proofs should be convertible:

The idea is that a counterexample to the theorem can be converted into a counterexample to a particular step (in Lakatosian terminology: a global counterexample can be converted into a local counterexample). The epistemic significance of convertibility, argues Easwaran, is that it allows rebutting defeaters (evidence against the truth of the theorem) to be turned into undercutting defeaters (evidence against the correctness of the proof). This is important because it means that if we learn that the theorem being proved is wrong, we can find out what went wrong with the proof and thereby correct, modify, or improve on it. Mathematically, this means that proofs must be written clearly enough to allow for convertibility. Once again, though, this proposed property of proofs is individualistic, standing against reliance on testimony in mathematics. The hypothetical “someone” in the quote from Easwaran above is still an individual, and the obvious application is to relatively short proofs, where one mathematician would be able to check the individual steps in the proof to see if a given global counterexample is also a local counterexample.

Having set out surveyability, transferability and convertibility, observe that these conditions are all modal conditions pertaining to what individuals could or would do with a purported proof.Footnote ¹¹ Modal claims are notoriously context-sensitive, and difficult to make exact, especially in the case of mathematics. For instance, the hypothetical failure of the theorem described in the convertibility condition will be mathematically impossible for all correct proofs, even if they are too brief to actually support the tracing of a hypothetical counterexample to a broken step in the proof. Giving defensible versions of these modal conditions is a considerable task, and we will not take it on here.

2.4. A social turn

A number of historians, sociologists, and philosophers of maths have developed accounts of the importance of social factors to mathematical practice.

In When Computers were Human, David Grier highlights the importance of collaboration to the production of mathematical tables, and human computing (Grier Reference Grier2005). Grier details a history of mathematical inquiry from the production of mathematical tables in post-revolutionary France to the human computers that worked in NASA in which collaboration – often at quite a large scale – was crucial to the production of mathematical knowledge.

Researchers have also stressed the importance of collaboration to contemporary mathematical practice. One major example of this is the online Polymath project, which involves large-scale online collaboration to solve mathematical problems. For instance, two big success cases are the new proof of the density Hales–Jewett theorem (Polymath Reference Polymath2012), and reducing the upper bound on gaps between primes (Polymath Reference Polymath2014a). Reflection by participants can be found in Gowers and Nielsen (Reference Gowers and Nielsen2009) and Polymath (Reference Polymath2014b). Researchers have taken an external interest in this too, using the Polymath project (and the related mini-Polymath) to study the social features of collaboration, such as in the work of Martin and Pease (Reference Martin and Pease2013) and Martin (Reference Martin, Felty and Middeldorp2015). They also study and model the social conventions that arose (Barany Reference Barany2010), the conversational patterns used in the online mathematics (Corneli et al. Reference Corneli, Martin, Murray-Rust, Pease, Puzio and Nesin2017), the use of explanation in mathematics (Pease et al. Reference Pease, Aberdein and Martin2019), and the kind of knowledge that is produced by Polymath projects (Allo et al. Reference Allo, Van Bendegem, Van Kerkhove, Aberdein and Dove2013). For a longer survey of the use of online mathematics to study mathematical practices, see Pease et al. (Reference Pease, Martin, Tanswell and Aberdein2020).

The significance of a social perspective on mathematics also has a firm root in sociological and ethnographic work on mathematics, especially situated within the field of Science and Technology Studies. For example, Mackenzie (Reference Mackenzie2001) writes extensively about proof and proving, beyond just mathematics to also include software engineering. For Mackenzie, mathematical “[p]roof, arguably, is intrinsically a public, social act” (Reference Mackenzie2001: 320). Following in this tradition are: examinations of gesture and materiality in mathematics (Greiffenhagen Reference Greiffenhagen2014), socio-historical studies of mathematical practice (Barany Reference Barany2016, Reference Barany2018, Reference Barany2020), and the ethnography of mathematical research centres (Lane Reference Lane2017).

Furthermore, the philosophy of mathematical practice also emphasises the practices of mathematics, and by extension social features of those practices. Overviews of the field can be found in Löwe (Reference Löwe, Ju, Löwe, Müller and Xie2016), Carter (Reference Carter2019) and Hamami and Morris (Reference Hamami and Morris2020). The major influence of the dialectical approach of Lakatos (Reference Lakatos1976)Footnote ¹² is evident in much of this area, and social features are explicitly present in major works such as Kitcher (Reference Kitcher1984) and Ernest (Reference Ernest1998). Some recent work includes applications of the tools of social epistemology to mathematics (Andersen Reference Andersen2017a, Reference Andersen2017b, Reference Andersen2020; Andersen et al. Reference Andersen, Andersen and SørensenForthcoming); a ‘dialogical’ conception of mathematical practice (Dutilh Novaes Reference Dutilh NovaesForthcoming); and group-level virtues for mathematics (Tanswell and Kidd Reference Tanswell and Kidd2020).

3.1. What does the theorem say?

Let us briefly set out what the Classification Theorem is and its importance.

In mathematics, a group is a set of elements G along with a binary operation * satisfying four axioms:

(Closure)

For all a, b ε G, a * b ε G. That is, the set of elements is closed under the binary operation: applying the operation to any two members will keep you inside the group.

(Associativity)

For all a, b, c ε G, (a * b) * c = a * (b * c). To illustrate, standard addition and multiplication both are associative, while subtraction and division are not. This is why there are groups with the former as their operation, but not the latter.

(Identity)

There exists an identity element id ε G such that for all a ε G, a * id = id * a = a.

(Inverses)

For any a ε G there exists a⁻¹ ε G such that a * a⁻¹ = a⁻¹ * a = id. That is, each element has an inverse within the group.

It is straightforward to show that each group has precisely one identity, and that each element has a unique inverse in the group. With these relatively simple axioms, group theory manages to identify a mathematically rich type of structure, with many properties and examples.

A group is finite if it has finitely many elements. A simple group is one whose only normal subgroups are the trivial, one-element group, and the group itself. Normal subgroups N are subgroups which are invariant under conjugation, which means: for all n ε N and g ε G, g * n * g⁻¹ ε N. The significance of this is that all groups can be thought of as being “built up” from simple groups, meaning finite simple groups are the basic building blocks of finite groups generally. Steingart (Reference Steingart2012: 190) draws the common analogy to prime numbers as the “building blocks” of the natural numbers, as for all numbers above 1 there is a unique prime factorisation.

The Classification of Finite Simple Groups is a theorem which states that all finite simple groups have been identified, as they are either an alternating group, a cyclic group of prime order, a group of Lie type, or one of the 26 “sporadic” groups. The sporadic groups are those that don't fit into the other categories, and include the well-known “Monster Group” with roughly 8×10⁵³ elements. Sometimes the Tits group is included as a 27th sporadic group, since it is not strictly speaking a group of Lie type, despite being closely associated with them. The interesting observation here is that even giving a precise mathematical statement of what the Classification Theorem says involves substantial mathematics, and so we will not expand on the contents of these categories further here.

3.2. The social proof

To understand the classification proof, one needs to understand its history in outline.Footnote ¹⁴ Ronald Solomon's history of the classification project starts in 1892, when Otto Hölder suggested that “it would be of the greatest interest if it were possible to give an overview of the entire collection of finite simple groups” (Solomon Reference Solomon2001: 315). Through the first half of the twentieth century, important progress was made by German and American mathematicians, but it was piecemeal, lacked general methods, and researchers largely worked alone. The Brauer–Suzuki–Wall theorem which was published in a jointly authored paper in 1958 (Brauer et al. Reference Brauer, Suzuki and Wall1958) was the result of convergent investigations, rather than a truly collaborative effort (Solomon Reference Solomon2001: 330).

In 1954, Brauer diagnosed the field as being in a state of stagnation, and tried to raise new interest in an address to the international congress of mathematicians. Adrian Albert saw the field as ripe for progress, and organised the Chicago group theory year in 1960–1, which brought together many mathematicians working on problems in group theory. This year allowed John Thompson and Walter Feit to collaborate intensively on the 255-page odd order theorem, and created a sense of group theory as an independent field (Steingart Reference Steingart2012: 191–5). The network of personal relationships established in this year was crucial to establishing working relationships, and through the 1960s and 1970s, group theorists collaborated intensively, producing co-authored papers at a much higher rate than their peers (Steingart Reference Steingart2012: 195). The complexity of the problems meant a slew of very long co-authored papers. Thompson (Reference Thompson1968, Reference Thompson1970, Reference Thompson1971, Reference Thompson1973, Reference Thompson1974a, Reference Thompson1974b), is 410 pages and comes in six parts; Walter (Reference Walter1967) is 109 pages; Alperin et al. (Reference Alperin, Brauer and Gorenstein1970) is 261 pages; Gorenstein and Harada (Reference Gorenstein and Harada1974) is 461 pages; and Aschbacher (Reference Aschbacher1977) is 115 pages. The difficulty of this work owes to the fact that the proof requires not only finding and describing all possible finite simple groups, but also showing that any group will fall into one of the 4 main group families, or the 26 sporadic groups. The process of discovering new sporadic groups is not systematic, and from the 60s to 80s, around 20 new sporadic groups were discovered (Steingart Reference Steingart2012: 190).

The network of mathematicians who contributed work to the proof was decentralised, with no managerial team, or clearing house for results. In all, the proof involved over a hundred mathematicians. The closest the project had to a manager was Daniel Gorenstein, whose 16-step plan proposed in 1971 (published in Gorenstein Reference Gorenstein1979: 182–93) gave structure to the later stages of the collaborative effort (Steingart Reference Steingart2012: 202). This network was tightly connected, and it was difficult for mathematicians who weren't plugged in to the system to systematically contribute (Steingart Reference Steingart2012: 197).

Group theorists began to reach a consensus that the project was coming to a close by the late 1970s (Solomon Reference Solomon2001: 340–1). In the preface to Finite Simple Groups: An Introduction to their Classification (Gorenstein Reference Gorenstein1982), Gorenstein announced that the proof had been completed in February 1981 (amended from a date of August 1980 in an earlier draft). This choice of date is a little difficult to understand, as at this point, many results were still in preprint. In any case it was incorrect, as there were several ‘gaps’ in the proof, the most important being the classification of the quasithin groups, which was completed by Aschbacher and Smith in a 1000-page two-volume monograph published in 2004 (Aschbacher and Smith Reference Aschbacher and Smith2004a, Reference Aschbacher and Smith2004b).

By the early 80s, efforts had already begun to construct a revisionist or second generation proof, which Gorenstein presents as aiming to eliminate so-called “local errors” in the proof, revise earlier papers in light of later ideas, and make clear how the different parts of the proof connect (Gorenstein Reference Gorenstein1980a: 4; Reference Gorenstein1980b: 8). At the time of writing, eight volumes of the second generation proof have been published with Gorenstein as a posthumous author (Gorenstein et al. Reference Gorenstein, Lyons and Solomon1994, Reference Gorenstein, Lyons and Solomon1995, Reference Gorenstein, Lyons and Solomon1997, Reference Gorenstein, Lyons and Solomon1999, Reference Gorenstein, Lyons and Solomon2002, Reference Gorenstein, Lyons and Solomon2004, Reference Gorenstein, Lyons and Solomon2018a, Reference Gorenstein, Lyons and Solomon2018b), and the authors estimate that the revisionist proof will run to eleven volumes (Ornes Reference Ornes2015: 75) and a mere 3,000 to 4,000 pages (Gorenstein et al. Reference Gorenstein, Lyons and Solomon1994: 3).Footnote ¹⁵ These volumes don't exhaust the second-generation proof, which relies on a number of ‘background results’. In addition Gorenstein (Reference Gorenstein1983) and Aschbacher et al. (2010) make up a shorter simplified presentation of the outlines of the proof, and the important properties of finite groups are described in the ATLAS of finite groups (Conway et al. Reference Conway, Curtis, Norton, Parker and Wilson1985).

In her excellent paper on the proof of the classification theorem (Steingart Reference Steingart2012), Alma Steingart draws attention to a number of shocking, epistemically important features of the proof.

The first is the sheer size of the proof, which earned the classification theorem the moniker “the enormous theorem”. When Gorenstein announced the completion of the proof, he estimated that the proof ranged between 300 and 500 papers, running to between 5,000 and 10,000 pages (Gorenstein Reference Gorenstein1980b: 1). When the first volume of the second-generation proof was published, the estimate crept up to between 10,000 and 15,000 pages (Gorenstein et al. Reference Gorenstein, Lyons and Solomon1994: 3). These estimates were of published papers, and don't cover the unpublished papers and ‘grey literature’ which either are or were at some point considered part of the proof.

The sheer size and complexity of the proof means that at no point could any individual claim to be in a position to validate the whole proof. No individual has read the entire proof (Solomon, quoted in Ornes Reference Ornes2015: 70), and no-one understands the proof in any depth (Davies Reference Davies2005: 1354). Very few even have a good claim to understanding how the proof hangs together. As a major force behind the planning of the first-generation proof and the revisionist efforts, Gorenstein was perhaps best placed to understand the whole, but the imprecision in his estimates of the size of the proof indicate the limits of his understanding.

The second feature is the importance of personal relationships to collaboration. Steingart stresses the interactive and personal features of the collaboration that went into the proof, including collaborations with emergent properties; the value placed on face-to-face collaboration and ‘kibbitzing’; and ‘non-textual means of transmission’, including mentorship, pedagogy, and exchanges of graduate students (Steingart Reference Steingart2012: 194–6). This high degree of collaboration created a fairly tight in-group which had access to pre-prints, techniques, and new results (Steingart Reference Steingart2012: 197).

The third feature is that, due to their complexity, many results were accepted despite reviewers and commentators being unable to understand them.Footnote ¹⁶ In 1970, Gorenstein, Alperin and Brauer published a 260-page paper in the Transactions of the American Mathematical Society (Alperin et al. Reference Alperin, Brauer and Gorenstein1970). In a commentary on the paper for Mathematical Reviews, Paul Fong (a student of Brauer) commented:

In a commentary on Walter (Reference Walter1969), Gorenstein made a similar concession: “The amount of notation involved and the author's expository style are such that the reviewer must admit that he has not read the argument in complete detail.” (Gorenstein Reference Gorensteinn.d.: MR0249504, cited in Steingart Reference Steingart2012: 200). We can't know for sure whether peer reviewers read the paper in full, but it certainly seems unlikely. Rather than being sceptical about these results, Steingart contends that in these cases the group theory community leaned on the credibility of the mathematicians to assuage worries about the proofs’ inscrutability, meaning that “personal trust, familiarity, and reputation became integral to the adjudication process” (Steingart Reference Steingart2012: 200). This trust involves what Wagenknecht (Reference Wagenknecht2014) calls opaque dependence, in the sense that mathematicians were unable to validate the results for themselves

The fourth feature is the sheer number of errors in the proof. A 1960 paper by Gorenstein and Walter was castigated for a host of “mathematical malapropisms” ranging from factual errors to bad notation in a review by Thompson (MR0177032, quoted by Steingart Reference Steingart2012: 198–9). John Walter – who made a number of important contributions to the proof – was notorious for making so-called ‘local errors’. A major challenge for the group theory community was to acknowledge the existence of these local errors, while maintaining the integrity of the overall proof (a theme we will return to in the next section).

The final shocking feature of the proof of the classification highlighted by Steingart is the concern that the theorem will be uninvented (Steingart Reference Steingart2012: 204–5). In Gorenstein's (Reference Gorenstein1983) introductory volume, he says:

In an article from 2015, Stephen Smith repeats this worry:

Drawing on Donald MacKenzie and Graham Spinardi's work on the uninvention of nuclear weapons (Mackenzie and Spinardi Reference MacKenzie and Spinardi1995), Steingart suggests that as group theorists who were involved in the project in the 1960s and 1970s die, the body of tacit knowledge on which the proof rests will be lost. Steingart mentions a number of distinct issues: that the mathematical community may collectively forget how to prove the classification theorem, that the loss of mathematicians who understand the way the different parts of the proof fit together undermines the status of the proof, and that the loss of mathematicians who understand the different parts of the proof will make “local” errors uncorrectable.

4.1. Can we know that the classification theorem is correct?

Above, we suggested that for someone to know a mathematical proposition, that proposition needs to be correct, believed, subject to epistemic support, and not subject to any undefeated defeaters. In the sense of knowing a proof that involves knowing that the theorem is correct, an agent need not have carried out the proof herself to know it; she can rely on epistemic support from the proof having been carried out correctly by others.

Group theorists have been fairly forthcoming about whether the classification theorem meets these conditions:

Feit claims both that the classification theorem is correct, and that its proof is ‘essentially’ correct. He also points out that group theorists have reached consensus about both issues. Presumably, he is appealing to conferences in Durham in 1978 and Santa Cruz in 1979, which seem to have functioned as consensus conferences (Solomon Reference Solomon2001: 340–1). It appears that the theorem is correct, and that many group theorists (and presumably other mathematicians) believe it.

Things get tricky with the epistemic support and no defeaters conditions. As we saw in Section 3.2., the proof of the classification theorem is known to be riddled with errors, and at least some group theorists are pessimistic about their capacity to detect errant sporadic groups (should any exist):

These concerns raise questions both about whether the proof provides adequate epistemic support for the theorem – you can't know a theorem based on an incorrect proof – and about whether the proof is subject to defeat. Even if the proof is in fact correct, the sheer length of the proof, the difficulty of the areas of mathematics it covers, and the unsystematic way in which sporadic groups have been discovered might act as defeaters, preventing a correct proof from grounding knowledge.

In the passage from Gorenstein, there are two moves made to address concerns about errors and missing groups: a shifting of the standards required by proof to allow what group theorists call ‘local’ errors, and an appeal to community checking in support of the claim that there are no missing sporadic groups (see also Aschbacher Reference Aschbacher1980: 64). Steingart also suggests that community checking mechanisms play a role in establishing that there are no non-local errors in the proof. Both moves essentially appeal to the community to provide epistemic support and defang defeaters.

Steingart presents the appeals to ‘local’ errors as a shift in the standards of proof:

Let's call this condition fixability. Like surveyability, transferability and convertibility, fixability is a modal condition. A proof is fixable when all of its errors could easily be corrected by experts within the relevant mathematical community, without needing to do any substantial new maths (a proof which has no errors will be fixable by default). Unlike surveyability, transferability and convertibility as traditionally conceived, the way Gorenstein and others deploy fixability involves appealing to the epistemic capacities of a mathematical community. No single mathematician could possibly fix all of the errors in the classification proof – it simply covers too many areas of mathematics – so the only sense in which it is fixable involves the group theory community. The fixability of the classification proof is a community-dependent property: one of the worries about the uninvention of the classification proof is that as group theorists active in the 60s and 70s die, the proof will no longer be fixable.

One problem with the concept of fixability is that it is unclear how to draw the distinction between ‘local’ and ‘non-local’ errors. A sceptic might maintain that allowing proofs to contain ‘local’ errors, without specifying the limits of this notion, is merely a rhetorical move that downplays the significance of errors. After all, allowing errors in a proof is a radical departure from the traditional conception of proof and would have further significant impacts on the status and reliability of the theorem.

What about the concerns that there might be non-local errors, and more sporadic groups lying in wait in the shrouded corners of mathematical possibility? Here's Steingart's take on how these worries were addressed:

Steingart is focused on non-local errors in this passage, but Gorenstein uses essentially the same reasoning regarding missing groups in the quote above (see also Solomon Reference Solomon2001: 347). Here Steingart presents the group theory community as appealing to what Sandford Goldberg calls coverage supported beliefs (Goldberg Reference Goldberg2010). Coverage-supported beliefs involve reasoning from the absence of evidence for some proposition, and the reliability and timeliness of one's sources of evidence on that subject-matter, to the conclusion that the proposition in question is false. This kind of reasoning is familiar from current affairs: we don't need to receive positive evidence that the United States is not at war with China to know that there is no such war, we can rely on the fact that if war had been declared, we would have heard about it by now. Coverage-supported belief can involve relying on a single individual (if a new episode of It's Alive! had come out, Laura would have told me about it by now), but usually it involves a more diffuse reliance on one's epistemic community and its ability to spread information in a timely manner. Goldberg argues that there are five conditions for X's coverage-supported belief that p in some subject-matter S to constitute knowledge:

1. (i) that there is some source Y who is disposed to report about S,

2. (ii) that Y is reliable about S,

3. (iii) that a sufficient interval has passed for Y to investigate whether p and pass on their discoveries,

4. (iv) that X has not received any report about p, and

5. (v) that X is receptive to reports from Y about S.

Goldberg's account is externalist in the sense that the agent employing coverage-reliability need not have evidence about the reliability of her sources, but we might want to add evidence of the fulfilment of some or all of these conditions as a condition of knowledge based on coverage-reliability.Footnote ¹⁸ In this case, the coverage is often even more extensive than Goldman's account suggests because many mathematicians have been looking. While any one of them could miss an error or gap, we might think that the group of mathematicians are unlikely to.

Group theorists are relying on coverage-reliability to support the belief that there are no more sporadic groups and that there are no non-local errors in the proof, providing evidence that the proof is correct, and a belief to defang relevant defeaters. Is this reliance legitimate? The answer partly depends on where you sit in the academic community. Someone who is ‘plugged in’ to the group theory community, receiving updates from list-servs, emails from colleagues, and from preprints will be able to rely directly on signals from the group theory community, with a low latency period for important discoveries, meaning that they will plausibly fulfil conditions (iii) and (v). A mathematician working in another branch of mathematics will have to rely on blogs, the testimony of colleagues in the know, or general-interest journals like the journal of the American Mathematical Society, which will have less space for discoveries in group theory, and a longer lag between discovery and announcements. A member of the public will end up relying on popular science journalism, which will be even less reliable at reporting developments in group theory, and will have a longer time between discovery and announcement.

Can someone working in group theory have sufficient coverage-reliability to know that there are no missing groups, and that there are no non-local errors? It's worth noting that Gorenstein, Feit, and Aschbacher were all writing around 1980, when the proof was not complete, and it is difficult to think of the missing 1000-page proof of the classification of the quasithin groups as anything other than a major error.Footnote ¹⁹ Although group theorists may have had justification to believe that there were no errors in the proof in 1980, they couldn't have known this. One important feature of coverage-reliability is that if a source continues to investigate a question, they can become more reliable over time, so at the current time group theorists may be in a position to know that there are no non-local errors or missing groups. This suggestion comes with some major caveats. It assumes that after 1980, members of the group theory community were reading and checking over hundred- and thousand-page proofs and trying to find new sporadic groups. It also assumes that they would have been willing to make their mistakes public (condition (i)). The discovery of a new sporadic group would certainly have been a publishable discovery, but errors in mathematics papers are not systematically published (rather the norm is to contact the author(s) to check whether an error is important). This suggestion also relies on the claim that the group theory community is sufficiently reliable at detecting errors and sporadic groups to ground knowledge (condition (ii)). A natural suggestion is that the revisionist proof will constitute a source on whether there are any non-local errors in the proof, but at the time of writing, the second-generation proof is far from finished, and it is an open possibility that writing the second-generation is taking so long because it requires fixing all of the non-local errors in the first-generation proof.

In this section, we've seen that individual knowledge that the classification theorem is correct is still importantly social, both in the sense that the proof that provides support for this belief is dependent on the group theory community's ability to correct local errors, and in the sense that this belief depends on the group theory community's coverage-reliability in detecting sporadic groups, and non-local errors in the proof. Whilst we've remained neutral about whether anyone is in a position to know that these problems do not arise based on coverage-reliability, this discussion has shown that even individual knowledge of the classification theorem is deeply social.

4.2. Who knows the proof?

In the previous section, we focused on individual propositional knowledge of the classification theorem, in which epistemic support was provided by the proof of the classification theorem, and considered the epistemic roles played by the group theory community. In this section, we turn to objectual knowledge of the theorem, and knowledge from proving activity. Objectual knowledge involves understanding a proof and knowing at least in outline how to carry it out. Knowledge from proving activity requires knowing how to prove a theorem, exercising this knowledge by actually carrying out the proof, and believing the theorem on the basis of this proving activity. We argue that to make sense of objectual knowledge of the classification proof, and the knowledge from proving activity, we must ascribe knowledge to the group theory community by exploiting the cumulative reading of a group knowledge ascription.

Can anyone claim to have objectual knowledge of the classification proof? We pointed out above that objectual knowledge ascriptions are gradable and that in some contexts, ‘understands the proof’ is fairly undemanding. We are not professional mathematicians – let alone group theorists – but there is a sense in which even we understand the proof: each of us can explain what the classification theorem means, and we know that Gorenstein's 16-step program lays out the rough shape of the proof.

Gorenstein's central role in the proof through the 1960s and 1970s means that he was probably best placed to understand the proof. However, his review of Walter's paper (MR0249504) demonstrates that he wasn't able to follow all of the papers in the proof. Steingart quotes from an interview with Gorenstein in 1981, who when asked about his inability to follow Walter's proof responded “I said I couldn't. Neither could the referee” (Steingart Reference Steingart2012: 200). At best, when the proof was completed (modulo the quasithin groups) Gorenstein and perhaps a few others (Davies Reference Davies2005: 1354 suggests a dozen) had a fairly detailed overview of the stages of the proof, knew which techniques they required, and knew which mathematicians had done each stage. None of the mathematicians knew how to use all of these techniques, or understand the shape of all of the sub-proofs in detail.

To find an agent that has objectual knowledge of the proof of the classification theorem in the demanding sense required by mathematical practice, we need to look to the group theory community. We assume that when the proof was finished in 2004, every mathematician who had contributed a proof to that effort understood their own proofs.Footnote ²⁰ They knew how to use the relevant techniques, understood the shape of their proof(s) and the key steps, and would have been able to teach other mathematicians the proof(s).Footnote ²¹ Similarly, although no individual had the connective knowledge of how the different proofs fit together (recall Gorenstein's uncertainty about which papers were part of the proof), between them the group theory community knew how all of the parts of the proof fitted together. If this situation obtained in 2004, the following sentence has at least one true reading:

The reading on which this sentence is true is not the distributive reading that ascribes objectual knowledge of the complete proof to every individual group theorist. Neither is it the collective reading that ascribes objectual knowledge to a robust group agent: the group theory community is not sufficiently internally coherent to count as a group agent with intentions and desires. Rather, the true reading appears to be the cumulative reading, which says that between them the group theory community has objectual knowledge of the complete proof, by its members having knowledge of parts of that proof.

The epistemic structure picked out by the cumulative reading of group knowledge ascriptions is discussed in Habgood-Coote (Reference Habgood-Coote2019a, Reference Habgood-Coote2020).Footnote ²² They argue that a sentence like ‘NASA knows how to make a space shuttle’ can refer to a fragmented state of knowledge, in which knowledge of the answers to different subquestions of how to make a space shuttle? are split between the different members of the group (for example, by the programmer knowing how to design the software, the chemist knowing how to make the fuel, and so on) and the answers to these subquestions cumulatively add up to an answer to the big question. We suggest that the group theory community's objectual knowledge of the classification proof has a similarly fragmented character. The big question is how to prove the classification theorem? which breaks down into smaller questions about the classification of different classes of groups like how to prove the classification of odd order groups? and how to prove the classification of abelian groups?. Gorenstein's 16-step program is a first pass at the way this question was broken up, but many of these steps will be further broken down into subsubquestions. The idea would be that the group theory community knows the classification proof in virtue of knowledge fragmented amongst the community. First, each of the contributing mathematicians knowing the answers to subquestions of how to prove the classification theorem?, knowing how to use suitable techniques, understanding their subproof(s), and being able to teach it to other mathematicians. And secondly, some of the mathematicians at the centre of the proof knowing how the different subproofs fit together (Habgood-Coote Reference Habgood-Coote2019a: fn. 34). These fragments include the tacit knowledge of the proof which Steingart suggests is in danger of uninvention, which in turn endangers the group knowledge if the fragments no longer add up to the full proof.

This cumulative account of group objectual knowledge lays the groundwork for an account of group knowledge from proving activity. Knowledge from proving activity involves correctly performing a proof by exercising knowledge of how to prove it, and then coming to believe the theorem on the basis of this proving activity. Knowledge of the classification theorem based on having proved it is a kind of group knowledge because both the proving activity was carried out by a group, and a group knew how to prove the classification theorem. The proving effort was a collaborative endeavour in two senses: a great many of the subproofs were collaborative (such as Feit and Thompson's proof of the odd order theorem), and taken together the subproofs constitute a collective intellectual endeavour, guided by Gorenstein's 16-step plan. Group theorists were not simply proving theorems because they thought they were interesting; they were proving theorems because of the community effort to prove the classification theorem. After 1960, group theorists took up problems precisely because they were required by the community effort, assigning problems to different mathematicians, and abandoning work when they realized that they were doubled up. There are also good indicators of a general belief that the theorem is correct in the group theory community: group theorists seem to have formed a consensus that the theorem is correct and its proof complete around 1980, and many mathematicians will happily cite the classification theorem in their proofs.Footnote ²³

The fact that it was the group theory community rather than any individual that proved the classification theorem does not mean that it is impossible for individuals to know the theorem, in the sense of knowing that the theorem is true. The situation is rather like that found in other large-scale scientific enterprises: the initial discovery of the Higgs boson was a group intellectual achievement involving the work of many hundreds of people,Footnote ²⁴ but when the discovery was announced in Science, readers of the announcement were in a position to know that the Higgs boson exists by relying on CERN. Similarly, we suggest that mathematicians and the public can know that the classification theorem is correct via testimonial reports, thereby relying on the collective endeavours of the group theory community.

4.3. What's the role of the second-generation proof?

With the discussion of the social epistemology of the classification theorem in place, we are in a position to circle back around to the second generation proof, and distinguish a number of different reasons why this effort is important for the epistemology of group theory. Gorenstein cites three reasons for the second-generation proof: correcting local errors, revising in light of new developments, and making clear how the proof fits together (Gorenstein Reference Gorenstein1980a: 4; Reference Gorenstein1980b: 8). We can now see that Gorenstein's estimation of the importance of the second-generation proof was overly modest: there are a number of further epistemic roles being played by this effort. These roles relate to the correctness of the theorem, whether the proof provides epistemic support, whether there are defeaters for the proof, and the status of the tacit knowledge involved in the proof.

The first and most significant issue is whether the classification theorem as stated is correct. Although there are coverage-supported reasons to think that there are no more that 26 sporadic groups, we've seen above that Solomon wouldn't rule out the possibility that there are undiscovered sporadic groups waiting to be discovered. One role of the second-generation proof is to check there are no more sporadic groups, and correct the statement of the classification theorem if there are.

The second issue is whether the proof of the classification theorem as it stood at the beginning of the 1980s lives up to the epistemic standards required for proof. If there are non-local errors in the proof, then it cannot provide epistemic support for belief in the classification theorem unless those errors are corrected. If there are local errors in the proof, but we include fixability as a condition on successful proof, the second-generation proof functions as a way to cash out the promise that there are only local errors in the proof. Correcting these errors also makes fixing the proof easier, opening up the possibility that the classification proof will remain a proof, even after the group theorists who worked on it leave the mathematical community. Correcting these errors thus blocks one of the possible routes by which the proof could be uninvented.

It is also possible that some of the efforts in the second-generation proof are aimed at ensuring that the classification proof is surveyable, transferable, and convertible. Although these standards might have been in the background of concerns about whether very long proofs could count as proofs, we think that these aims are unlikely to be fulfilled, given the size and complexity of the second-generation proof. We will return to this in the next section.

The third issue is whether the mere possibility of non-local errors and undiscovered groups functions as a defeater for knowledge of the theorem. Even if the proof is error-free, and the description of groups is complete, the mere existence of these possibilities may be enough to prevent knowledge of the theorem. Responding to these concerns, we might think of the second-generation proof as functioning something like a massive double-checking exercise that aims to buttress the coverage-reliability of the group theory community in their beliefs that all groups have been described, and all non-local errors in the proof corrected.

The final issue is what will happen to the knowledge involved in the proof effort that hasn't managed to make its way into the journals as mathematicians start to leave the group theory community. This includes tacit knowledge relating to techniques and ideas employed in the proof, understanding of the overall shape of the proof, and what Aschbacher calls ‘well-known’ theorems which have never been written down, presumably because they were common knowledge in the group theory community at the time of the first-generation proof.Footnote ²⁵ Steingart suggests that writing down the unwritten parts of the proof was crucial to its status:

Without writing down the ‘well-known’ theorems, mathematicians could only know the theorem by taking the word of the group theory community that all of the relevant theorems are known, and writing down these results and getting them into print solidifies the proof into a permanent object which can claim to be part of mathematical knowledge, even after its authors die (Bird Reference Bird2010). Unlike unwritten theorems, the know-how and understanding relating to the proof cannot be solidified by being put into print. This knowledge plays two roles: it was a necessary component in the group effort to prove the classification theorem, and it is crucial in ensuring that the proof is fixable by the group theory community. If the proof is in fact correct, and is fixable by mathematicians who haven't spent decades working in group theory, the loss of this know-how wouldn't mean that the theorem would no longer be known, but the proof would no longer be understood. In Gorenstein's words, the proof would be lost to ‘the living world of mathematics’. By writing down the entire proof in an accessible way, the architects of the second-generation proof can ensure that future generations are at least in a position to know and understand the classification proof. Although it may not be important to reprove the classification theorem from first principles, the major role of group theory in pure mathematics means that there would be a significant loss if the techniques and ideas employed in the classification proof were to pass into obscurity.

To sum up: the most important functions of the second-generation proof are to (i) provide greater coverage reliability for the proposition that there are no missing groups or other non-local errors, (ii) to defang defeaters for the classification theorem, (iii) to write down and record unwritten proofs and (iv) to put future generations in a position to know and understand the classification proof.

4.4. Collectivising surveyability, transferability, and convertibility

Having examined the Classification Theorem and its epistemic status at some length, let us return to the nature of proof to draw some conclusions about the social turn that is needed in characterising important properties that proofs have.

Recall the properties of surveyability, transferability and convertibility. These, we argued, were all characterised as primarily individualistic properties of proofs (even though they are connected to social features). We contend that, in order to make sense of the Classification theorem, we face a trilemma. We must either abandon these kind of criteria as necessary features of proofs; collectivise these features; or deny that the Classification Theorem has been proven.

Abandoning these criteria is an option; surveyability in particular is already controversial. The upshot then is that we would need to reconsider the responses to computer-assisted and probabilistic mathematics that motivated them in the first place. Doing so would not be independent of the work we have done here, as it would still involve issues of testimony, reliability, and the epistemic role of proofs.

Rejecting the proof is also possible. Indeed, the mathematician Kevin Buzzard explicitly points to the Classification Theorem as a case where scepticism may be warranted:

We do think that the worries that have been discussed about size, local errors, and uninvention are enough for Buzzard to be justified to raise these concerns.

Nonetheless, for the mathematicians who want to defend the Classification Theorem as a proof proper, we believe that collectivisation presents a path to updating the conditions like surveyability, transferability and convertibility. Indeed, in considering the Classification Theorem, we already encountered fixability as an example of a potential property of proofs which is collectivised. Let us now consider what collectivisation would mean for our other three properties.

Recall that a proof is surveyable if it can be checked and understood as a complete whole. Obviously, the enormous proof is not surveyable in the individualistic sense: no mathematician can check the whole thing, and certainly cannot understand it as a complete whole. However, we can consider ways in which this surveyability may be possible at the group level instead. Bassler (Reference Bassler2006) distinguishes between global and local surveyability, where global surveyability is being able to see how the whole proof hangs together, while local surveyability is being able to survey each of the individual steps in some order. Local surveyability can be collectivised on the cumulative model above: the task of surveying the individual steps or subproofs is fragmented across individual mathematicians, and so between them they can cumulatively survey all of the steps. For global surveyability, we once again note the fragmented character of the proof being made up of many subproofs, subquestions and different papers. The key then is that this permits global surveyability of those subproofs by different individuals. When combined with other individuals who understand how these subproofs can be brought together to form the proof of the Classification Theorem, the understanding of the completed whole is cumulative amongst the group, and between them they might satisfy global surveyability. (Of course, whether all of this understanding is actually in place for the enormous proof is an empirical matter, and thus whether it has been globally surveyed is too. But surveyability is a modal notion, so this is beside the point.)

Turning to transferability, that a relevant expert would become convinced of the truth of the theorem just by consideration of each of the steps in the proof, again the enormous theorem would fail this due to the human limitations on the relevant expert. Nonetheless, we can collectivise transferability to mean that a relevant expert community would become convinced of the truth of the theorem just by consideration of each of the steps in the proof. The mechanisms for doing so would also work on the fragmented model of group states, where distributed fragments would convince relevant experts, assuming those fragments add up to the whole proof, and between them they would be convinced of the theorem proved. Importantly, this still makes the same predictions on probabilistic proofs that motivated Easwaran (Reference Easwaran2009).

Finally, let us consider convertibility, where if a counterexample were to be discovered, it could be traced to specific errors in the proof. Given that understanding the proof of the Classification Theorem requires a community of mathematicians, it follows that tracing where a counterexample is the result of an error or gap in a proof also requires a community of mathematicians. A collectivised notion of convertibility would state that a hypothetical counterexample could be traced by the community of mathematicians to the proof step(s) that failed.

The original proposals for these three properties were that they were describing existing (though possibly implicit) features of mathematical practices. We contend that the individualistic presentations of these properties, though, are actually just the simplest cases of the collective practices. In fact, it is these collectivised notions we have just described that are already implicit in mathematical practices. There are many long proofs, or difficult areas of mathematics that are challenging to even the experts working in them, where such collectivised properties of proofs are what underlie the practices of proving.