I know Godel's theorems state that there exist mathematical statements which are true but not provable. I am concerned here with provably true mathematical statements whose "minimal" proof length makes a proof impractical in the real world.
Does there exist a theorem which can be described with $N$-bits, where $N$ is relatively small (e.g., small enough that said theorem written in this form can be reasonably read by a human), which is provable within some standard axiomatic framework (say ZFC), but whose minimal proof length $M$ is sufficiently large that a proof within our physical universe is impossible (say $M \gg 10^{100}$)?