In provability logic, $\square X \rightarrow X$ is not a theorem.

In my head[1] this reads as "if X is provable you don't necessarily have a proof of X".

This has lead to the question, what does provable even mean, if not there exists a proof of X? Is there an example of some proposition that is provable but does not have a proof?

Please help

^[1] I come from type theory so I tend to think constructively.