Is truth futureproof? On the possible futures of mechanized proofs