1. Polite Applause

On July 22, 1976, Kenneth Appel and Wolfgang Haken announced a proof of the four-colour theorem. A planar map, with the usual assumptions on regions, can be coloured with at most four colours so that regions sharing a boundary segment receive different colours. Merely touching at a point does not make two regions neighbours.

At the joint American mathematical meetings in Toronto that August, Haken presented the result to a crowded audience. A problem open for 124 years appeared to be settled.

Donald Albers, who attended, later described a surprising response. He had expected an eruption of celebration. What he heard was polite applause, followed by mathematicians expressing unease.

The proof included roughly 1,200 hours of computer calculation. No realistic human reader could reproduce every computation by hand. Perhaps an error lay somewhere in the output. Albers wondered whether some listeners were almost hoping one would be found. His account appeared in 1981, several years after the lecture; it reports the reception rather than preserving a contemporaneous transcript.

The theorem itself barely requires a minute to explain. In 1852, Francis Guthrie noticed while colouring an English county map that four colours seemed sufficient. Through his brother Frederick, the question reached Augustus De Morgan, who wrote to William Rowan Hamilton on October 23.

De Morgan's uncertainty was part of the message: a student had asked for a reason for a purported fact whose status De Morgan himself did not know. Hamilton replied three days later with a pun about a quaternion of colours and little enthusiasm for taking up the problem. His own quaternions had occupied him since 1843.

Francis Guthrie, twenty-one and completing his legal education, did not build a research career around the conjecture. He later moved to South Africa, taught mathematics for many years, and studied Cape plants with Harry Bolus. A botanical name commemorates him alongside the mathematical problem.

The distance between an easily understood question and its proof was already remarkable. Toronto exposed a further distance: the gap between having an argument and being able to hold all its verification within one person's work.

That concern had a particularly uncomfortable precedent. The four-colour problem had already possessed an accepted proof—and lost it.

2. A Proof That Lived for Eleven Years

In June 1878, Arthur Cayley asked the London Mathematical Society whether anyone had settled the map-colouring problem. The following year Alfred Kempe, a barrister who had studied mathematics with Cayley, announced a proof in Nature and published the full argument in the American Journal of Mathematics.

Its central device was ingenious. Consider connected regions coloured with just two colours. Swap those colours throughout an appropriate connected chain and the colouring can remain valid while making room elsewhere. Such structures became known as Kempe chains.

The proof was accepted for eleven years. Peter Guthrie Tait also offered related approaches containing valuable ideas and fatal errors. The problem seemed finished to many readers.

In 1890, Percy Heawood found the defect in Kempe's treatment of a region with five neighbours. The argument required successive recolourings that were assumed to behave independently. They need not: one change could destroy the conditions required for the next.

Heawood salvaged a weaker theorem. Five colours always suffice. Kempe chains survived too, becoming durable tools in graph theory.

The episode is not unusual because an incorrect proof contained good mathematics. Failed arguments often leave useful methods. What is striking is the duration of collective confidence in a short enough, readable enough proof.

Readability does not establish that a sufficient check has actually occurred. A proof may sit before eminent mathematicians for years without its crucial weakness being exposed.

Heawood remained interested in colouring for almost six more decades, publishing on it into old age. His Durham career included service as vice-chancellor. Recollections of the slight figure, enormous beard, old cloak, and classroom dog supply a person behind the correcting lemma, though they do not add evidence to the proof itself.

The lesson cuts in two directions. A machine calculation does raise questions about software and hardware. But a human-readable text has never carried an automatic certificate of correctness simply because a person could, in principle, read it.

Toronto's unease therefore cannot be answered by choosing an immaculate human tradition over a newly fallible machine. Fallibility was present on both sides. The question was how each kind of argument could acquire reliable scrutiny.

A proof that lasted eleven years showed the difference between potential surveyability and actual examination. A proof with thousands of machine hours made the difference impossible to ignore.

3. Inside the Illinois Computer Room

Heinrich Heesch had developed crucial ideas for a computational attack before Appel and Haken. During the 1960s he pursued reducibility and discharging, using computers to test local configurations. Haken consulted him in 1967, and Heesch's subsequent American visits connected him with larger machines and collaborators.

Funding was a practical constraint, not a footnote. The withdrawal of German support limited work at an important stage. Haken later described discouraging advice from computing experts about the feasibility of the approach.

Appel disagreed. He believed computation could do the job if the project had enough time and careful organization. Their sustained collaboration began in 1972, with Appel concentrating on computation and Haken on the structural argument.

The machine was not summoned at the end to check a few arithmetic details. Human rules and computational results formed a repeated cycle. Proposed rules generated tests; failures prompted revised rules; new tests exposed further cases. The final proof was produced through that interaction.

Accounts distinguish different stages and different lists. Numbers commonly reported include 487 discharging rules, roughly ten thousand manually considered local cases, and about two thousand configurations subjected to computational tests. Total machine time was around 1,200 hours. Their own estimate of logical operations was on the order of ten billion.

Computing time came from actual institutional equipment, including a machine acquired for university administration in March 1976. A theorem depended partly on gaining access to resources bought for other work.

The manual labour also extended beyond the named authors. Dorothea Haken helped inspect configurations. Before publication, children from both families compared diagrams and printed output: Dorothea and Armin Haken, and Laurel, Peter, and Andrew Appel.

Laurel, thirteen, checked hundreds of pages. Haken later recalled hundreds of discrepancies she found and corrected, with the remaining problems repaired by the principal authors. Such reminiscences concern transcription and checking; they should not be transformed into a claim that the theorem survived hundreds of unrepaired mathematical counterexamples.

The list changed as the proof was organized. The preprint's 1,936 configurations became 1,482 in the published version, with further reductions in later presentations. The 1977 papers included John Koch as a coauthor on the reducibility part and were accompanied by extensive microfiche material. Appel and Haken later produced a book-length account in 1989.

Checking all the output for even a difficult single configuration could consume years of full-time human work, by their estimates. No ordinary referee could simply repeat the experiment with pencil and paper.

Meanwhile, the department's outgoing mail acquired a celebratory postmark: four colours suffice. The institution could stamp the conclusion in a moment. Explaining the machinery of confidence took much longer.

4. Why There Was a List

Suppose a counterexample exists. Choose one of minimum size. Every smaller relevant map or planar graph then admits a four-colouring.

The proof seeks two properties of a finite set of local configurations. First, the set is unavoidable: every graph satisfying the conditions imposed on a minimal counterexample must contain at least one listed configuration.

Second, each listed configuration is reducible: it cannot occur in a minimal counterexample. A suitable reduction yields a smaller graph; a colouring of that graph, combined with the reducibility argument, can be extended or rearranged to colour the original.

The contradiction is immediate once both large tasks are complete. The supposed minimal counterexample must contain a listed configuration, yet cannot contain any of them.

Unavoidability is established through discharging. Assign numerical charges using vertex degrees and the constraints of a planar embedding. Move charge according to carefully designed local rules. The total and the possible final distributions force some listed pattern to occur.

Kempe's older argument began with a short unavoidable list: in a suitable planar graph, some vertex has degree at most five. Vertices of sufficiently small degree can be handled. The degree-five case was where the claimed four-colour proof failed.

Heesch and his successors replaced an inadequately controlled case by more elaborate configurations whose reducibility could be tested separately. Elaborating the patterns increased the number of boundary colourings that had to be considered.

The scale is not captured by simply counting diagrams. A configuration can have a surrounding ring with many possible colour assignments, even after equivalent assignments are identified. Rings of fourteen or eighteen vertices already lead to hundreds of thousands or millions of relevant possibilities, depending on the precise counting convention.

The computer made this style of proof feasible. That does not establish that every conceivable proof of the theorem must use a long list or a machine. It explains why the particular strategy they successfully developed required computational help.

The argument's conceptual skeleton is intelligible: minimal counterexample, unavoidable configuration, reducibility, contradiction. Its verification load is enormous.

This separation becomes important in the later philosophical dispute. Someone can understand why the architecture works without personally checking every instance. Conversely, exhaustive checking alone does not necessarily provide a satisfying explanation of why four, rather than five or six, is the decisive number.

A proof can be transparent at one scale and opaque at another. Calling it simply readable or unreadable loses that distinction.

5. Three Different Uneasinesses

The objections fell into at least three kinds.

One questioned whether such an argument counted as a proof in the traditional sense. In 1979, philosopher Thomas Tymoczko emphasized surveyability: a proof should be available to a person's comprehensive inspection, not merely support conviction through a trusted computation. Accepting the four-colour argument, he suggested, expanded the concept of proof.

A second objection accepted its validity but wanted explanation. The result was established through a vast case analysis; why should four colours be enough? A shorter or more illuminating proof might answer a different intellectual need.

A third asked how errors could be detected. Was the program correct? Was the list complete? Had diagrams or data been copied wrongly? Did the computation actually implement the intended mathematical test?

Richard DeMillo, Richard Lipton, and Alan Perlis argued in 1979 that mathematical reliability also depends on social processes: criticism, simplification, reuse, and teaching. Formal validity as an ideal is not a description of all the work through which a community comes to trust a proof.

Later developments addressed this third concern most directly, without automatically settling the other two.

Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas initially sought to check the earlier proof but found the task unwieldy. They produced a new proof, announced in the mid-1990s and published in its full form in 1997. Their unavoidable set contained 633 configurations, with thirty-two discharging rules. Programs and data were made available for others to run.

The improvement did not remove computers. It made the dependence simpler and more reproducible. Their research announcement states the theorem in its precise planar-graph form.

In 2005, Georges Gonthier completed a formal proof in Coq, with Benjamin Werner involved in its development. It followed the modern proof route, not a retrospective certification of every original Appel–Haken program. A relatively small logical kernel checked formal derivations, including justified computation.

Trust was concentrated rather than abolished. The foundational rules, checker implementation, execution environment, and correctness of the formal theorem's interpretation still mattered. But one no longer had to trust a large special-purpose calculation in exactly the same way.

A March 2026 preprint by Inoue, Kawarabayashi, Miyashita, Mohar, Thomassen, and Thorup proposed a near-linear-time colouring algorithm and a new proof using 8,202 reducible configurations. The authors' text explicitly gives that number, including two elementary cases. This is the authors' preprint claim, not a new computer-free proof. As of this review on 1 October 2026, it should not be presented as a result already established by long-term independent community scrutiny; that caution is not evidence that it is wrong. A faster algorithm can require a longer configuration list.

Correctness, practical reproducibility, and explanatory satisfaction have not collapsed into one criterion.

6. A Theorem Too Large for a Book

The classification of finite simple groups presents a different kind of scale.

A group has an associative composition operation, an identity, and inverses. A simple group has no nontrivial proper normal subgroup. The word “normal” is essential: simple does not mean having no subgroups at all.

Finite groups can be analysed through composition series whose factors are simple. This resembles factoring integers into primes, but the analogy has limits. Knowing a group's simple factors does not uniquely determine how they are assembled.

The most elementary simple groups are cyclic groups of prime order. The five rotations of a regular pentagon form one. The smallest nonabelian simple group has sixty elements: A5, also realized by the orientation-preserving symmetries of an icosahedron. Its role in the nonsolvability of S5 connects the classification's subject to the general quintic equation.

The classification lists infinite families and twenty-six sporadic exceptions. The largest sporadic group is the Monster, whose order has fifty-four decimal digits.

Bernd Fischer and Robert Griess predicted it in the early 1970s. Griess announced a construction in January 1980, published in 1982 under the name “friendly giant.” The associated 196,883-dimensional algebra supplies its structure: the Monster acts as its full automorphism group, not merely as the arbitrary symmetries of an unspecified high-dimensional space.

Even individual components of the classification were enormous. Feit and Thompson's 1963 paper occupied 255 pages and proved that every finite group of odd order is solvable. It does not say that every odd-order group is nonsimple: cyclic groups of odd prime order are simple. The consequence is that every nonabelian finite simple group has even order.

A team led by Gonthier formally verified a proof of the odd-order theorem in Coq, reporting the achievement in 2013. Their paper describes six years of work and substantial reusable mathematical libraries.

The entire classification spans hundreds of papers and roughly a hundred major contributors. Estimates of ten thousand or fifteen thousand pages depend on which background results count as part of the proof. There is no single natural boundary around its documentary extent.

Daniel Gorenstein supplied a broad organizing view across decades. By the early 1980s, introductory accounts treated the programme as complete. Specialists believed the major branches were covered and the remaining work under control.

But “experts know how the remaining case should be finished” is not identical to “a complete, published, checkable argument is available.” The difference between those sentences concealed a serious gap.

7. The Missing Part

The quasithin case formed a substantial branch of the classification. Geoffrey Mason announced relevant results around 1980 and produced a manuscript of roughly eight hundred pages. It was not published as a completed proof and ultimately proved insufficient.

There was no single dramatic day on which a Heawood pointed to one bad line. The inadequacy became clearer as the classification's dependencies were revisited during the late 1980s and 1990s. A region generally regarded as closed was not actually closed in the public proof.

Michael Aschbacher and Stephen Smith supplied a new treatment in two volumes published in 2004, together about 1,220 pages. This was not a one-page erratum. It was a large mathematical project needed to complete a major piece of the argument.

Three claims can therefore coexist. The classification list was broadly accepted as correct by the early 1980s. The first-generation proof literature had a serious unfinished component. The 2004 work provided a complete treatment of that component.

Gorenstein had already recognized that even a correct first-generation proof would be an unsatisfactory final exposition. With Richard Lyons and Ronald Solomon, he began a second-generation presentation designed to clarify the organization and reduce dependence on scattered papers.

He died in August 1992. The first volume appeared in 1994. A tenth volume appeared in 2023, and the broader rewriting programme, including work associated with Gernot Stroth, continued beyond it. Precise counts and completion forecasts should be dated to their sources rather than treated as timeless descriptions of a moving project.

The purpose of rewriting is not merely literary elegance. A coherent exposition exposes missing hypotheses, unclear dependencies, and places where a result has been trusted without an adequate available argument.

No documented claim establishes that one person has checked every line of the first-generation proof together with every result on which it relies. Several mathematicians possess an extraordinary command of the overall structure. That is different from personally auditing every page.

The community's actual method does not require a superhuman reader. Specialists examine regions of the proof. Results are reused, compared, and occasionally challenged. Reuse creates opportunities for checking, not a guarantee that every citation triggers a complete audit. Gaps require repair; major gaps require substantial new work.

Surveys and systematic monographs turn a network of personal confidence into a more explicit network of mathematical dependencies. They cannot make all expertise reside in one head, but they can make it easier for different people to test different links.

A community can know a theorem without any individual possessing every detail. The credibility of that knowledge depends on the structure and accessibility of the distributed work.

8. Three Kinds of Finished

Kepler's sphere-packing conjecture supplies a third example.

In his 1611 essay on the six-cornered snowflake, written as a New Year's gift, Kepler proposed that familiar close packings of equal spheres achieve the greatest possible density in three-dimensional space. The arrangement resembles oranges stacked at a market.

The history also runs through cannonballs and Thomas Harriot's work for Walter Raleigh. Harriot corresponded with Kepler from 1606. Hilbert later included sphere-packing questions within his eighteenth problem.

Thomas Hales announced a proof in 1998, with Samuel Ferguson responsible for an important part. The argument combined theoretical reductions with inequalities, linear programming, and finite computational checks.

The Annals of Mathematics assembled a referee group of roughly a dozen people. Years of scrutiny produced substantial confidence but not a complete certification of every computation. Gábor Fejes Tóth's often-quoted “99 percent” assessment was an expression of that practical confidence, not a formally calculated probability that the theorem was true.

Hales's Annals paper appeared in 2005, on pages 1065–1185—121 pages, not exactly one hundred. It presented the main argument while computational material and related work had their own publication arrangements. The journal record makes the dates and extent checkable.

Hales then organized Flyspeck, a formal-verification project. Instead of asking referees to accept the computational parts as trusted black boxes, the project reconstructed a proof in formal systems. Completion was announced on August 10, 2014. The published account appeared in 2017 with twenty-two authors, using HOL Light and Isabelle. The formal paper states that scope.

One theorem thus has several completion dates: the authors' announcement in 1998, journal acceptance and publication in 2005, completed formal verification in 2014. None makes the others fictional. Each answers a different institutional and epistemic question.

Earlier episodes asked retrospectively what should count as axiomatization, proof, or calculus. Here contemporaries asked whether an argument already before them had become secure knowledge.

Defenders of computer-assisted proof objected that mathematics had never required all background knowledge to fit simultaneously into one person's mind. A twenty-page paper may depend on thousands of earlier pages. Length alone cannot supply a principled boundary.

William Thurston's 1994 discussion of proof and progress emphasized another aim: helping human beings understand and think mathematically. That goal is not identical to checking a derivation, though neither need exclude the other.

The central change is therefore not a simple transfer from humans to machines. Logical validity, human understanding, and practical checkability have become conspicuously separable.

The four-colour theorem exceeded ordinary human capacity through computation. The classification exceeded it through literature and specialized knowledge. Formalization tries to express dependencies in a form that a checker can follow step by step.

This answers much of the question of reliability, under stated assumptions. It does not automatically answer why a result feels illuminating. A mathematical community can have excellent grounds for knowing a conclusion while still seeking a better explanation.

What one person cannot hold may be organized into parts that different people—and independent checkers—can inspect.

The next episode follows a different consequence of computational asymmetry. In 1977, three researchers at MIT proposed an encryption system built around the ease of multiplying large primes and the apparent difficulty of reversing the operation. A company and a patent would follow.