new from me, @etosch , @cxli , and Elan Semenova: "Is truth future-proof? On the possible futures of mechanized proof". contains provocations, philosophical framings, and accounts of current practices in light of the idea that mechanized proofs contain mathematical knowledge that we might want to persist across future generations.
preprint: khoury.northeastern.edu/~cmart…
presented at PLATEAU a few weeks ago. slides: khoury.northeastern.edu/~cmart…
chris martens
in reply to chris martens • • •one of the outcomes of this work i want to highlight is the observation that not everyone mechanizes proofs for the same reasons. there are motivations that derive from:
- *Convincing*: wanting to improve confidence in results as objects of study scale in complexity;
- *Explaining*: wanting to improve precision and clarity in definitions, communicate ideas, and identify reusable abstractions.
a lot of talking past each other can happen when we conflate these purposes
chris martens
in reply to chris martens • • •another line of thought that emerged (and appears more significantly in the talk slides than in the paper) is how the desire to future-proof proofs participates in the broader human project of cultural artifact archival, alongside the history of media forms like film, games, net art, etc. and their respective challenges and changes to the technical needs of archives.
also, how stewardship matters. the work of re-transcribing and re-situating old work is how we express our care for its value
chris martens
in reply to chris martens • • •chris martens
in reply to chris martens • • •