When Proofs No Longer Need to Be "Understood": A Paradigm Revolution at the Bedrock of Mathematics

**By PeterZou**

In the Kuhnian sense, an improvement within a paradigm optimizes parameters inside the old definition; a paradigm revolution replaces the standard for "what counts as a question and what counts as a good answer."【verified·classic literature】

Applied to proof, this essay relies on just two specific criteria: **Has the warrant of the proof changed? Has the locus and identity of the reasoning changed?**

| Question | Old-paradigm default | Deepening | Revolution |

To understand this revolution, we must first see what props up the old "human-centered view of proof":

**A1 The social-persuasion thesis.** The essence of proof is an argument that "convinces a qualified human reader," and its validity is warranted by the community's deliberation, citation, reproduction, and acceptance. In *On Proof and Progress in Mathematics* (1994), Thurston argued that what mathematicians actually transmit is "understanding," and that formal proof is merely one means of communication; Lakatos's *Proofs and Refutations* (1976) went further, describing it as a fallible, revisable socio-historical process.【verified·classic literature】

**A2 The subject-ownership thesis.** Reasoning is a mental and normative process carried out in consciousness by a reasoner qua subject; the one who executes it and the one who warrants it are the same accountable person.【inference】

**A3 The discovery–justification division of labor.** In *Experience and Prediction* (1938), Reichenbach established a dichotomy: conjecture and inspiration belong to the "context of discovery," while rigorization and verification belong to the "context of justification"; machines excel at the latter, and the former is human territory.【verified·classic literature】

**A4 The formalization-as-supplement thesis.** Ordinary proofs are "semi-formal," abbreviated arguments, and Coq/Lean formalization is merely a "translated copy" of the proof, not the thing itself. The Four Color Theorem (Appel–Haken 1976; formalized by Gonthier in Coq in 2005) and the Kepler conjecture (Hales 1998; 12 referees spent four years and would only say they were "99% certain"; later formalized by the 20-person Flyspeck project) were both treated as "special cases."【verified·classic literature】

**A5 The bivalence-and-finality thesis of certainty.** A proposition either has a proof or it does not, and once a proof is accepted, the matter is settled; Gödel's incompleteness (1931) was treated merely as a "technical limitation."【verified·classic literature】

Together, these five props uphold the entire apparatus of peer review, journals, citation networks, tenure, and reputation. When the foundation moves, everything above it shakes.

**M1 | The warrant migrates from "consensus" to the "checker kernel."** Liquid Tensor Experiment: Scholze issued the challenge in December 2020, and the Lean community completed formal verification of the main theorem on liquid vector spaces on July 14, 2022.【verified】 The Equational Theories Project, initiated by Tao and others in September 2024, established on April 14, 2025 the 22,028,942 implication relations among 4,694 equational laws, all formalized in Lean.【verified】 The implication is clear: for the first time, "being true" can be adjudicated by an algorithm on an auditable basis of trust, and the "justification" in JTB-style knowledge is rewritten as "machine-checkable warrant."

**D1 | A proof is a two-layer object.** The thing itself is no longer "a text" but [an independently checkable formal object] + [a narrative explanation aimed at understanding]. The two layers can be produced separately and audited separately.【inference】

1. **Treat "verifiability" as a first-class citizen of product design.** Rather than arguing about whether AI's conclusions are right, design a replayable, auditable verification chain. The capacity to warrant is the trust asset of the next generation.

The most counterintuitive thing about this revolution is that it does not require us to believe in AI first. On the contrary, it replaces the question of "whom to believe" with "can it be independently checked." As the warrant migrates from human consensus to a replayable checker, mathematics — humanity's oldest and hardest fortress of certainty — is the first to show what the next generation of trust infrastructure looks like.