Looking from the inside and from the outside

Many times in mathematics there is a natural dichotomy between describing some object from the inside and from the outside. Imagine algebraic varieties for instance; they can be described from the outside as solution sets of polynomial equations, but one can also try to understand how it is for actual points to move around inside them, perhaps to parameterize them in some way. The concept of formal proofs has the interesting feature that it provides opportunities for both perspectives. The inner perspective has been largely overlooked, but in fact lengths of proofs lead to new ways to measure information content of mathematical objects. The disparity between minimal lengths of proofs with and without ``lemmas'' provides an indication of internal symmetry of mathematical objects and their descriptions. A principal observation of this paper is that mathematical structures can be embedded into spaces of logical formulae and inherit additional structure from proofs. We shall look at finitely-generated groups, rational numbers and SL(2,Z), and examples from topology and analysis.