In recent years there has been a movement to collaborate on math proofs via blueprints (dependency graphs) in the Lean language, which seems related.

For example:

https://teorth.github.io/equational_theories/

https://teorth.github.io/pfr/

thanks, these are interesting indeed!