# Information density of proofs?

I am a CS person so please excuse the hand-waving.

Given a set of machine-represented proofs, each different (but not necessarily proving a different thing), what sort of information-theoretic statements could we make about these?

I would define the information "density" of a proof by simply losslessly compressing it using some standard means (like lz4 or rle or whatever is suited to this domain) and comparing the compressed size to the input size. The compression ratio.

For example: if we compress them all, would they all have similar compression ratios (meaning non-redundant/repeating information content)?

Given a set of different proofs, all proving the same thing (say like the prime number theorem), what is the most dense? The least dense?

Are there useful proofs that are not "information dense", meaning they have long repeating sequences or repeating structure that is easy to compress. These would look tedious to a human but would be discover-able by a machine.

Are there any papers that have looked at this? What area is this? My googling has failed me.

First, beware: this can only be done meaningfully within a fixed "language of proof". If you try to compare across different systems, you can get wildly different results. There is a whole domain of Proof Complexity which has lots of results about "expressivity". Adding features to your language (like let x = <big-expression> in <other-expression>) can make a huge difference. Other subtler changes can still result in exponential differences in proof length.