More accurately, it's a repository of placeholders where the formalised mathematics might eventually be put.

I had a quick flip through it and most of the interesting things are just "sorry", which is the Lean equivalent of "throw new NotImplementedException();"