Math talk: Theorem about git revision control system? I would like to give a mathematics talk on the git revision control system. It is now widely used in mathematics as well as in the computer science industry.  For example, the HoTT (Homotopy Type Theory) community uses it, and it is the go to system for collaborative editing of text files, whether they be source code or latex markup.

I know git uses the notion of a directed acyclic graph, which is a start.  However, a good mathematics talk mentions proofs and theorems.

What theorem might I prove about git that is actually relevant for its use?
Interestingly, there is a nascent mathematisation of version control systems, although at this point it's only partially applicable to Git. It's called patch theory [1, 2, 3, 4, 5] and  arose in the context of the DARCS version control system. It can be seen as an abstract theory of branching and merging. Recently patch theory has been given HoTT [ 6 ] and categorical [ 7 ] treatments. 

Patch theory is work in progress, and doesn't cover all aspects of version control, but contains a lot of theorems that you could look at. It is a clear example of theory that's applicable to the 'real world' -- not surprising, for patch theory is an abstraction / simplification of something very concrete. At the same time it connects with cutting-edge maths like HoTT.




J. Dagit, Type-Correct Changes - A Safe Approach to Version Control Implementation.
G. Sittampalam, Some properties of darcs patch theory.
I. Lynagh, Camp Path Theory.
D. Roundy, Implementing the darcs patch formalism ... and verifying it.
J. Jacobson, A Formalization Of Darcs Patch Theory Using Inverse Semigroups.
C. Angiuli, E. Morehouse, D. R. Licata, R. Harper, Homotopical Patch Theory.
S. Mimram, C. Di Giusto, A Categorical Theory of Patches.