It doesn't mean anything. The point is that the language of lean, and its proof derivation system, are able to express (and prove) statements that do not correspond to any meaningful mathematics.