Proof Assistants and Social Epistemology

Proof assistants and social epistemology examines how the use of formal proof assistants — such as Coq, Lean, Isabelle, and HOL Light — transforms the social and epistemic norms of mathematical practice. When a proof is checked by a machine rather than by a human referee, the locus of epistemic authority shifts from individual expert judgment to the transparency of the verification algorithm and the reliability of the software stack.

This shift raises profound questions. If no human can read a ten-thousand-line formal proof in its entirety, does the mathematical community know the theorem, or does the community merely trust the software? The phenomenon of delegated verification — where epistemic authority is transferred from human agents to computational systems — is not unique to mathematics. It mirrors the broader transformation of knowledge production in an age of machine learning, big data, and algorithmic decision-making. Understanding how proof assistants reshape the sociology of mathematical knowledge provides a model case for studying how automation changes epistemic norms across disciplines.

See also Mathematical Knowledge and Delegated Verification.