Proof in the time of machines

2023/05/03 by Granville, Andrew
#FOS: Computer and information sciences #FOS: Mathematics #History and Overview (math.HO) #Logic in Computer Science (cs.LO) #Number Theory (math.NT)

paper · doi:10.48550/arxiv.2305.02329

Abstract

We compare the values associated with (traditional) community based proof verification to those associated with computer proof verification. We propose ways that computer proofs might incorporate successful strategies from human experiences.

Related

• Can Computer Programs be Formally Verified?
• Mathematics in the Age of the Turing Machine
• Computer Runtimes and the Length of Proofs: On an Algorithmic Probabilistic Application to Waiting Times in Automatic Theorem Proving
• Automatic verification and interactive theorem proving
• Accepted proofs: Objective truth, or culturally robust