Computer-Assisted Proofs in Philosophy: The Four Color Theorem as Methodological Precedent

This paper explores the legitimacy of computer-assisted proofs as a methodological framework in philosophy, using the Four Color Theorem as a historical precedent. Following Appel and Haken’s 1976 proof and its later Coq formalization by Gonthier, it argues that formally verified reasoning—once controversial in mathematics—can equally transform philosophical analysis. As a case study, a Coq formalization tests interpretations of Pratītyasamutpāda (dependent origination) against classical identity axioms, showing a logical collapse when dependency erases distinction. The result is not an exegetical claim about Buddhism, but a proof-of-concept for “formal metaphysics”: applying machine-verifiable logic to clarify metaphysical commitments. The study situates philosophy within the same epistemic evolution mathematics underwent when computer proofs gained acceptance.