Is truth futureproof? On the possible futures of mechanized proofshttps://khoury.northeastern.edu/~cmartens/papers/plateau26-itfp.pdf
Interactive theorem provers play increasingly important roles in the programming languages and mathematics communities, resulting in a large body of mechanized proofs that bear witness to mathematical knowledge. The ideal promise of accumulating these artifacts is that they allow us to preserve that knowledge across time into future generations and across intellectual silos. However, by virtue of being software, mechanized proofs are at risk of breaking as they age, hindering reproduction (e.g. of the proof’s correctness), inspection, and reuse. How can we future-proof mechanized proofs? In…