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();"
1 comment
[ 3.7 ms ] story [ 16.8 ms ] threadI had a quick flip through it and most of the interesting things are just "sorry", which is the Lean equivalent of "throw new NotImplementedException();"