Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ ZENODOarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Report . 2026
License: CC BY
Data sources: ZENODO
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
ZENODO
Report . 2026
License: CC BY
Data sources: ZENODO
ZENODO
Report . 2026
License: CC BY
Data sources: Datacite
ZENODO
Report . 2026
License: CC BY
Data sources: Datacite
ZENODO
Report . 2026
License: CC BY
Data sources: Datacite
versions View all 3 versions
addClaim

Truth After Proof: Formal Epistemics in Modern Mathematics

Authors: Jefferson, Bob;

Truth After Proof: Formal Epistemics in Modern Mathematics

Abstract

This work examines how the relationship between proof, verification, and truth functions in contemporary mathematics. As mathematical arguments have grown in scale, abstraction, and formal sophistication, the classical ideal—according to which a proof is a finite object that can, in principle, be fully surveyed by an individual—no longer provides an adequate description of how mathematical certainty is actually established in practice. The manuscript introduces formal epistemics as a descriptive framework for analysing this situation. Rather than questioning the objectivity or rigor of mathematics, it investigates the architecture of justification: where mathematical certainty resides, how it is justified and distributed, and what principled limits constrain it. The analysis is structured around three canonical case studies: Fermat’s Last Theorem, illustrating exact truth sustained by large-scale proofs, distributed verification, and transitive trust within an expert community. The Prime Number Theorem, illustrating asymptotic truth, where a rigorously proved universal claim has content that is expressed through limiting behaviour rather than finite instantiation. Gödel’s incompleteness theorems, illustrating a principled boundary of formal closure, where true statements exist that cannot be proved within the formal systems that express them. Formal verification and proof assistants are treated neither as remedies for these features nor as sources of epistemic crisis, but as tools that clarify them by making dependencies, assumptions, and boundaries explicit. The work argues that modern mathematics has not lost rigor, but that rigor now takes multiple, structurally distinct forms. The manuscript is intended for philosophers of mathematics, logicians, mathematically literate philosophers of science, and mathematicians interested in the epistemology of proof and formal systems. This Zenodo release constitutes Version 1.2, considered stable, submission-ready, and suitable for archival reference. Future versions, if any, will be limited to minor typographical or presentational corrections.

Keywords

Gödel incompleteness, Fermat's Last Theorem, mathlib, epistemology, Lean, philosophy of mathematics, proof theory, formal verification, prime number theorem

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Green