Formalized Mathematics: Proofs and Reusable Libraries

A checked theorem is useful on its own. A library of compatible definitions and theorems changes what can be built next.

Formalized mathematics therefore has two intertwined histories: the completion of demanding individual proofs and the construction of reusable mathematical infrastructure. The second history explains why later projects become possible without rebuilding every foundation.

Before the famous milestones

Automath's formalization of Landau's analysis text and Mizar's sustained library development established substantial precedents in the 1970s and afterward.

Other assistants accumulated developments in arithmetic, algebra, analysis, and computer science. The field did not begin when a well-known theorem first received a widely publicized formal proof.

These earlier projects encountered recurring problems: representing mathematical structures, handling implicit arguments, choosing convenient definitions, and making a lemma usable outside the proof for which it was first written.

An account centered only on record-setting theorem names misses much of the work that made formalization sustainable.

Computer assistance and formal checking

Kenneth Appel and Wolfgang Haken's 1976 proof of the Four Color Theorem relied on substantial computer calculations. John Koch contributed to the computational work.

The proof became a focal point for questions about what it means to inspect a mathematical argument when some calculations are too extensive to check by hand.

Georges Gonthier's later formalization, developed with Benjamin Werner and completed in 2005, provided a different assurance structure in Coq. It used a formal combinatorial treatment and checked the connection between the theorem and the computational reasoning.

This was not simply running the 1976 program again. Formal verification required proving that the encoded objects, reductions, and checking procedures established the stated mathematical result. Gonthier's 2008 account, “Formal Proof—The Four-Color Theorem,” explains the mathematical organization.

The distinction remains useful: a computer-assisted proof and a proof checked within an explicit formal system can share substantial computational work while making different claims about how that work is justified.

Reflection and verified computation

Suppose an expression language represents polynomial identities. A normalization program computes a canonical form, and a theorem proves that normalization preserves the expression's mathematical meaning.

To prove

the system can normalize both sides and establish that the resulting representations agree.

The logical justification has two components: the correctness theorem for normalization and the specific calculation on these expressions.

This is the principle of proof by reflection. Instead of constructing a long sequence of low-level rewrites afresh, the proof invokes a verified computational procedure.

The trust boundary depends on how computation is performed and checked. Kernel reduction, verified certificates, and externally executed code accepted through additional mechanisms do not automatically provide identical guarantees.

Reflection helped make some large formal developments practical. It also illustrates how proof theory, computation, and implementation design meet inside a single proof.

The Odd Order Theorem

The Feit–Thompson theorem states that every finite group of odd order is solvable.

Gonthier and a substantial team formalized a proof in Coq, completing the development in 2012 and publishing the main account in 2013. The project paper records a collaborative effort involving algebraic infrastructure, proof methodology, and extensive mathematical development.

The theorem's importance here is not only its length or fame. Its formalization required coherent representations of finite groups, algebraic structures, character theory, and many supporting constructions.

The Mathematical Components approach, including small-scale reflection, made those structures and reasoning patterns reusable. Contributors such as Assia Mahboubi, Enrico Tassi, Cyril Cohen, Laurent Théry, and the other coauthors belong in the account alongside the project's lead.

A library architecture is itself a mathematical achievement when it lets independently developed results fit together without repeated translation.

Flyspeck and the Kepler conjecture

Thomas Hales's proof of the Kepler conjecture combined mathematical reasoning with extensive computation. The Flyspeck project sought a formal verification of the argument.

The collaborative formalization was completed in 2014. Its paper appeared as a preprint in 2015 and in final journal form in 2017, dates that refer to different stages of the same project.

The development used HOL Light and Isabelle for different parts, with computational checks and mathematical reductions linked through formally justified arguments. The project paper documents the result and its many contributors.

Flyspeck illustrates the need to coordinate several kinds of evidence: continuous mathematics, discrete classification, inequalities, and extensive computation. It also demonstrates why a formalization's architecture can differ from the organization of an informal published proof.

Hales's later critical retrospective discusses the project's costs and lessons. Formalization can improve assurance while still imposing substantial work in representation, tooling, and maintenance.

What an ordinary theorem depends on

Consider the elementary statement that a group has a unique identity element.

Let $e$ and $e'$ each satisfy the appropriate identity laws. Then

The proof is short. Its formal setting still needs a carrier type, a multiplication operation, equality, and the relevant identity hypotheses.

If the theorem is stated for an existing group structure, the library must determine which multiplication is intended and which identity laws are available. Implicit arguments or type-class inference may fill in that information.

If one proof treats a group as a bundled object and another treats the carrier and operations separately, a bridge may be needed before their lemmas compose conveniently.

The kernel ultimately sees explicit mathematical data. The surface notation's convenience depends on a carefully designed elaboration and library layer.

This small example explains why a library's usefulness cannot be measured simply by counting theorems. Compatibility and discoverability affect whether a result can be reused.

Mathlib and community infrastructure

The Lean mathematical library, Mathlib, developed as a community project with a shared collection of definitions, proofs, and supporting tools.

The community-authored library paper describes its aims and organization. A separate maintenance study examines technical and social challenges as the library grows.

Contributors do more than add theorem statements. They review definitions, generalize lemmas, maintain naming conventions, improve automation, update dependencies, and repair proofs after changes.

A more general theorem can make many later proofs shorter, but excessive abstraction can make a library harder to use. Those are mathematical design choices made through collaboration and review.

The same lesson applies beyond Mathlib. Mizar, Isabelle's Archive of Formal Proofs, Mathematical Components, HOL libraries, and other collections provide different models of organizing shared formal knowledge.

Checking the statement

Mechanical checking establishes a derivation of the formal statement. It does not by itself establish that the statement captures the intended theorem.

Suppose an informal theorem concerns all continuous functions on a compact interval. A formal version might accidentally quantify only over polynomials, omit a nonempty-domain condition, or use a topology different from the intended one.

The resulting proof could be completely correct for that different statement.

Review must therefore inspect definitions, hypotheses, quantifier order, and the relationship between informal and formal formulations. An axiom report can reveal additional assumptions, but understanding whether those assumptions are appropriate remains mathematical work.

Proof, explanation, and social review

Richard De Millo, Richard Lipton, and Alan Perlis's 1979 critique emphasized the social processes through which mathematical proofs gain acceptance and questioned ambitious claims about program verification.

Later formalization achievements answer some practical doubts about scale. They do not make explanation, communal understanding, or specification review unnecessary.

A machine-checked proof can offer highly detailed evidence of derivability while remaining difficult for a person to understand. A clear mathematical exposition can explain the idea while leaving routine inferences implicit.

These forms of evidence can support one another. The strongest practice connects the formal artifact with an intelligible statement, an explanation of the argument, and a record of its assumptions and dependencies.

Formalization and discovery

Formalizing a known theorem can discover missing hypotheses, new abstractions, or alternative arguments. It does not automatically constitute the first discovery of the theorem itself.

A library can also support new mathematics by making a body of results precisely searchable and composable. This possibility depends on the quality of the library and the methods used to explore it.

Before examining learned proof search, one further foundational development deserves its own explanation: the interpretation of equality as higher-dimensional structure.

Sources and further reading

• Kenneth Appel and Wolfgang Haken, Four Color Theorem papers and announcements (1976–1977), including computational work with John Koch.
• Georges Gonthier, “Formal Proof—The Four-Color Theorem” (2008); formal proof distribution.
• Georges Gonthier and collaborators, “A Machine-Checked Proof of the Odd Order Theorem” (2013).
• Thomas Hales and collaborators, “A Formal Proof of the Kepler Conjecture”, preprint 2015, journal publication 2017.
• Thomas Hales, “The Formal Proof of the Kepler Conjecture: A Critical Retrospective” (2024).
• The mathlib Community, “The Lean Mathematical Library” (2020).
• “Maintaining a Library of Formal Mathematics” (2020).
• Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis, “Social Processes and Proofs of Theorems and Programs” (1979).