This isn't necessarily true.

While every formal proof can be encoded mathematically that doesn't imply that the grammar of lean or rocq is sufficient to encode every potential proof.

However the core of what you are saying: that every possible proof exists in the space of all mathematical statements is correct.