Your comment reminds me of Gödel's proof of his incompleteness theorem. Basically, he said that if you treat a mathematical statement as a sequence of tokens, a

Your comment reminds me of Gödel's proof of his incompleteness theorem. Basically, he said that if you treat a mathematical statement as a sequence of tokens, and then assign a number to each token, then you can transform the statement into a big number. Then, going one step further, if a mathematical proof is a sequence of statements then it can be too transformed into a really long number. Then you can come up with rules to manipulate these numbers to create new valid statements and proofs. I don't know if there was much work done on this idea beyond Gödel's proof, but I think it's a really neat idea that gives a way to manipulate mathematical proofs as objects and create new ones from a very high level view.