Theorising about a structure behind proofs made of an alphabet isnt new - its part of theorems like Godels Incompleteness, etc.

Actually exploring or evaluating objects in this space has always (and continues to be) intractable due to the high complexity and computational power required.