Mastodawn

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: https://khoury.northeastern.edu/~cmartens/papers/plateau26-itfp.pdf

presented at PLATEAU a few weeks ago. slides: https://khoury.northeastern.edu/~cmartens/talks/plateau-itfp-talk-slides.pdf

Show thread

chris martens 2d ago

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

Show thread

chris martens 2d ago

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

Show thread

chris martens 2d ago

people shouted out in the talk include @ionchy for their lovely reproduction of Reynolds' "types, abstraction, and parametric polymorphism", @MartinEscardo for his posts about Agda as communication tool, and @david for letting me ask annoying questions about his Lean projects :)

Show thread

chris martens 2d ago

PLATEAU is a workshop, so this paper is mostly a discussion starter that gestures towards possible projects (we aren't describing a new solution or advocating for a particular agenda). i really want to hear from more folks about your answers to the discussion questions at the end, or any other feedback!

Show thread

chris martens 2d ago

one more point i'll add to this thread is that distinguishing *mechanization* from *formalization* makes a difference in how we reason about the social and mathematical meaning of proof, and contemplating archival/preservation of proofs only reinforces the importance of this difference.

not all formalization efforts are mechanized, and not all mechanization efforts are formal!

Show thread

Meven Lennon-Bertrand 1d ago

@chrisamaphone Lots of food for thought in this work, thanks a lot!

I've been recently doing some necromancy to bring back from the dead a 10+ years old Rocq library, which I found to be a very interesting experience… I haven't exactly sorted my thoughts out yet, but I'm planning to write about it soon, and some of it will for sure be part of the conversation you're trying to have!

Show thread

Meven Lennon-Bertrand 1d ago

@chrisamaphone (One tiny thing about the LF-for-interoperability aspect: on this side of the Atlantic the Dedukti people have been and are still very active about it. It's not perfect, but they've achieved quite a bit of cool results and translations!)

Show thread

chris martens 17h ago

@mevenlennonbertrand ah that's cool; is there a website for the project or should i just poke around at what i'm finding on arxiv and github? who are the active people these days?

Show thread

Meven Lennon-Bertrand 15h ago

@chrisamaphone You can probably start by looking at the webpage of Deducteam, the main team active on it atm: https://deducteam.gitlabpages.inria.fr/

Deducteam

Show thread

Meven Lennon-Bertrand 1d ago

@chrisamaphone Also, one of my main motivation for mechanisation is not "external" but "internal": I don't mechanise to convince or explain to others, but to understand, ie chiefly for myself. This can be for both existing results I want to get a grip on, techniques I want to understand enough to apply to a problem I work on, or new ideas the ITP is helping me develop. I guess you could view this as a variation of the explaining though, but directed towards me rather than anyone else? Especially since once finished this sort of work tend to lean more of the explaining side than the convincing: now that I have explained to myself, I can try to do so to others.

Show thread

chris martens 16h ago

@mevenlennonbertrand yes, this is a big motivation for me too! actually i think both convincing and explaining can be self-directed: for the convincing case, for example, i can delegate some amount of scrupulousness in checking my own proofs

Show thread