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 inte

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();"