Executive Summary

This white paper explores the epistemological and practical question of how we can know whether all corollaries and “obvious” proofs have been derived from a given set of mathematical theorems. In doing so, it evaluates the limitations of human mathematical intuition and tradition-bound exploration methods, and the emergent role of formal systems and proof assistants in systematically uncovering and verifying mathematical truths. Special emphasis is given to how proof assistants such as Coq, Lean, Isabelle/HOL, and HOL Light contribute to the identification of low-hanging theoretical advances—those corollaries, lemmas, or special cases that are provable with existing machinery but often remain unpublished or unexplored due to oversight, tradition, or lack of systematization.

1. Introduction: The Problem of Theoretical Exhaustion

In the history of mathematics, there has been a long-standing question of when a theory or subfield can be considered “complete” in the sense that all direct implications and corollaries of a given result or framework have been adequately explored. While mathematicians routinely speak of “trivial” or “obvious” consequences, the identification and cataloging of these consequences is not guaranteed, nor systematically pursued across all fields.

This paper addresses two interrelated questions:

How can we know whether all obvious consequences of a theorem have been proven? To what extent can formal systems and proof assistants help to systematically uncover such consequences?

2. Human Mathematical Practice: Intuition, Oversight, and Incompleteness

2.1 The Fallibility of Mathematical Intuition

Mathematical development has traditionally relied on human pattern recognition, problem-driven inquiry, and communal consensus about what is worth proving. This results in significant blind spots:

Obvious results may be dismissed without proof. Minor corollaries may be left unpublished. Intermediate results may be rediscovered independently.

2.2 Historical Examples of Overlooked Corollaries

Numerous historical examples underscore the incompleteness of human mathematical exploration:

Gauss’s Lemma in number theory was implicit in earlier work but remained unstated until later. Simple special cases of Gödel’s incompleteness theorem were often left out of standard logic textbooks. Matrix identities and inequalities, such as those used in control theory and quantum mechanics, are often rediscovered across disciplines.

2.3 Mathematical Publication Bias

Journals prioritize novelty and often reject results considered “trivial” or “obvious,” leaving many foundational or low-hanging results unpublished or undocumented. This leaves significant gaps in theoretical closure.

3. Formalization: From Theorem to Corpus

3.1 What Formalization Entails

Formalization refers to the process of expressing mathematical definitions, theorems, and proofs in a machine-checkable format, within a formal logical system. Proof assistants such as Coq, Lean, and Isabelle/HOL are used to:

Define axioms, structures, and theorems. Derive lemmas and corollaries through mechanized logic. Verify the consistency and correctness of proofs.

3.2 The Role of Type Theory and Logical Foundations

Proof assistants rest on formal logical foundations—typically variants of type theory or higher-order logic. This enforces rigor and enables exhaustive exploration of definitional consequences. For example, in dependent type theory (as used by Coq), every function and theorem must be precisely typed, forcing clear definitions and enabling proof automation.

4. Proof Assistants and the Discovery of Low-Hanging Theoretical Advances

4.1 Corollary Mining via Proof Assistants

Once a set of definitions and theorems are formalized, proof assistants can be used to:

Automatically search for logical consequences, via tactics or automation tools. Prove standard lemmas that have never been formalized before. Detect gaps or inconsistencies in existing “informal” literature.

This makes it possible to mine a theory for “obvious” or implied results that would otherwise be overlooked.

4.2 Examples in Practice

The Lean Prover Community’s mathlib has uncovered dozens of useful lemmas and identities in algebra, topology, and category theory that were not widely documented in textbooks. HOL Light’s formalization of real analysis discovered clean derivations of several classical theorems. Formal verification of the Four Color Theorem and Feit–Thompson Theorem revealed the intricate dependency of many “obvious” lemmas previously glossed over.

4.3 Automating Proof Discovery

Automated tools such as:

Sledgehammer (Isabelle) Tactician and GPT-f (Lean/Coq) Proverbot9001 (for Lean)

… are now capable of suggesting intermediate steps or even full proofs based on pattern recognition and past proofs. This can surface hidden connections and expedite the formalization of corollaries.

5. Epistemological Framework: When is a Theory “Exhausted”?

5.1 Local Closure vs Global Exhaustion

Theoretically, local closure refers to proving all results that are direct syntactic consequences of a set of axioms or theorems, whereas global exhaustion includes all semantically meaningful or practically useful consequences.

Even with proof assistants, semantic relevance remains a human-guided concept. Thus, we can say that:

Proof assistants can certify syntactic completeness (within formal boundaries). They cannot replace human valuation of relevance, elegance, or pedagogical utility.

5.2 Finiteness and Decidability

In many mathematical domains, especially in first-order logic over finite structures, all logical consequences are recursively enumerable. But for domains such as real analysis or set theory, completeness is undecidable, and exhaustiveness must be approximated by heuristic or human-guided methods.

6. Practical Obstacles to Full Formalization

6.1 Time and Labor Cost

Formalizing existing results is labor-intensive, often requiring 5–20x the time of writing a traditional informal proof.

6.2 Ambiguity in Informal Mathematics

Informal proofs often rely on tacit assumptions, ambiguous notation, or implicit appeal to prior knowledge, all of which must be made explicit for formalization.

6.3 Tooling and Community Fragmentation

Different communities use different proof assistants, creating silos that hinder the global accumulation of formalized knowledge.

7. Recommendations

7.1 Formalization as Standard Practice

Encourage mathematics departments and journals to adopt formalization of key results as a component of publication and research. A “formal appendix” may become a norm for high-value results.

7.2 Funding and Infrastructure

National science agencies and grantmakers should fund:

Development of more powerful automation tools. Expansion of standard libraries in formal systems. Collaborative repositories that reward contribution to formal proof corpora.

7.3 Education and Cultural Change

Introduce proof assistant use in undergraduate curricula. Promote cultural legitimacy of formalization and corollary mining as intellectually valuable pursuits.

8. Conclusion: Formalization as Epistemic Insurance

The use of proof assistants provides a form of epistemic insurance: guaranteeing that nothing trivially provable is left unproven, and offering a systematic framework for discovering overlooked truths. While they cannot replace human mathematical creativity or value judgment, they can greatly reduce blind spots and redundancy. For domains such as algebra, topology, and even physics-informed applied mathematics, their ability to reveal low-hanging theoretical advances may mark a new era in mathematical completeness.

References

Gonthier, G. (2008). Formal Proof—The Four-Color Theorem. Notices of the AMS, 55(11), 1382–1393. Avigad, J., et al. (2020). A Survey of Lean Usage in Mathematics. arXiv:2001.09382 Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge University Press. de Moura, L., & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. arXiv:2109.10059 Wiedijk, F. (2007). The QED Manifesto Revisited. Studies in Logic, Grammar and Rhetoric, 10(23), 121–133.