How do you save your proof for eternity?

Stream: lean4

[Mr Proof]

If I have written a proof in Lean 4, it may use some tactics like "simp" and "ring_nf"

In a 100 years nobody will know what this means.

So when I save my proof, I would need to save not only the proof but definitions of every function and tactic I used, in a human readable AND computer readable way.

What are the best ways to save your proof for eternity that a future human will be able to reconstruct your proof, even if the Lean language is forgotten to time?

[Henrik Böving]

Many lean proofs are written in such a way that they are split up into a myriad of individual statements that are easy to show on their own. The Lean proofs that exist in mathlib right now are not optimized for human readability either.

[Mr Proof]

I see. But my point is, if I wanted to save my proof and put it on a USB stick for future generations. I would have to also save a copy of Mathlib and also the Lean software. Or at least a specification of the Lean software?

e.g. if my proof contained something like "simp;ring_nf;rw[<-sqrt_sq]" and then in Lean 4.1 the definitions of those things changed my proof would no longer work.

I mean I could just write a proof and after every line write "this is easy to show". But then is it really a proof anymore?

So I'm just wondering about future-proofing-proofs.

[Ruben Van de Velde]

The way this currently works is that your project specifies explicitly what version of lean and dependencies it uses, and even if things change in lean 4.1, you keep using the version that works

[Johan Commelin]

Mr Proof said:

I see. But my point is, if I wanted to save my proof and put it on a USB stick for future generations. [...]

Stick it on github. It's arctic code vault will most likely survive your usb stick.

[Kim Morrison]

I'm not sure that either usb sticks or arctic code vaults are really in the right direction.

[Kim Morrison]

It's reproducible builds, and people caring, that gets you there.

[Damiano Testa]

And "for eternity" seems overly ambitious.

[Utensil Song]

For eternity, it's indeed reproducible builds, and people caring, assuming we manage to survive the Great Filters ahead of us, and we run CI across the galaxy.

For post-apocalyptic scenarios, it would seem reasonable to vendorize and freeze everything that your proof depends on in a Github repo except for the bootstrap stuff already available in arctic code vault (see How do you handle repositories with dependencies, like libraries? What about build system? Will you archive everything needed to build my repository? in this FAQ and this list of the stuff you don't need to archive, e.g. clang compiler but we need lean-llvm anyway). It's reasonable to assume that people need many years to recover to a state to care about mathematical proofs, and by then they would have already recovered quite some other useful stuff (e.g. a Github, and many other dependencies) from the arctic code vault.

[Martin Dvořák]

Mr Proof said:

e.g. if my proof contained something like "simp;ring_nf;rw[<-sqrt_sq]" and then in Lean 4.1 the definitions of those things changed my proof would no longer work.

This is why you shouldn't use simp nonterminally.

Ultimately, however (no matter how many good code practices you follow), you will also have to preserve the version of Lean and Mathlib you depend on.