In recent years there has been a movement to collaborate on math proofs via blue...

		marvinborner 3 months ago \| parent \| context \| favorite \| on: Determination of the fifth Busy Beaver value 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!