The consequences of bitrot are not contained in the domain of the system administrator. Here’s Mario Carneiro on the state of a formal, computer-checkable proof of a mathematical theorem:
I was blown away when I discovered that Isabelle’s proof of the prime number theorem was done in Isabelle2005, and it was not upkept along with the AFP (archive of formal proofs). Moreover, apparently not even the creators know how to run Isabelle2005 anymore, and everything has changed since then so it’s not backward compatible by any stretch. Basically, the proof is lost at this point, and they are more likely to formalize an entirely different proof than upgrade the one they already have.
Meanwhile prose proofs dating back to the 1800s are still good. Though time will presumably destroy those too, if they are not “upkept”. Languages evolve and go extinct. Books are destroyed.
No comments:
Post a Comment