[markmiro]

If these proofs really are like codebases, wouldn't we eventually expect these proofs to be written as software?

You'd install lemmas using a package manager and then import them into your proof.

You can then install updates to proofs. Maybe someone has found the proof to be wrong, in which case you either find a different proof or invalidate the lemma so all the dependents can be invalidated automatically.

[anyfoo]

That is not too far from what proof assistants actually do.

Agda is a dependently typed language (strongly resembling Haskell in Syntax, but with a lot more Unicode) where you rarely, if ever, "run" your programs but rather just check if they "compile", i.e. type check. If it does type check, you proved what you set out to prove.

Its standard library contains a lot of stuff you'd need for basic proofs: https://agda.github.io/agda-stdlib/

[HighlandSpring]

And the individual lemmas could have author and chronology metadata attached, then you could plot the DAG as a roadmap/tech tree of sorts with an axis corresponding to time.

You'd be able to at a glance see the year a result entered public domain, who authored it, etc

One can dream

[clcaev]

Creating an extensive library of formally verified results is the goal of many systems, such as http://metamath.org/

[jstogin]

I have wondered this as well. In theory, I want to say yes. But in practice, at least in this subfield, there are so many unimportant details that might make this really difficult.

It's not a perfect analogy, but some parts of the proof feel more like neural networks than procedural algorithms. So instead of verifying the composition of two procedural algorithms g(f(x)), you have something more like g(nn(f(x))), where nn is some sort of ML model / neural network. Interestingly, we are starting to see progress in importing ML models as libraries (eg Huggingface), so maybe that can carry over someday? I don't know.

Another challenge is simply a practical one. You would need someone heavily interested in both black hole mathematics and formal proof verification to be able to do this. Both of these require years of training.

[remolueoend]

The isabelle AFP project (https://www.isa-afp.org) might be interesting to you.

[barking_biscuit]

And then you can learn about a hip new javascript front-end framework for your proofs every month on HN.

[kapv89]

Checkout leanprover