  One often sees a sharp distinction in mathematics between descriptions from
the outside and from the inside. Think of defining a set in the plane through
an algebraic equation, or dynamically as the closure of the orbit of some point
under iterations of a given mapping. In logic one sees this dichotomy in the
descriptions of sets of tautologies through semantics and proofs. Logic
provides several tools for making outer descriptions of mathematical objects.
  This paper concerns a slightly complicated mixture of themes related to inner
descriptions and formal proofs. We use the notion of feasibility to embed
mathematical structures into spaces of logical formulas, from which we can
obtain new structures through proofs. We present new geometries on finitely
generated groups through proofs, and new structure on the rational numbers (or
other fields) which is susceptible to dynamical processes, such as the action
of $SL(2,Z)$ by projective transformations. We consider the topological notion
of {\em Serre fibrations}. This entails more difficulties of formalization, but
basic points arise already for {\em torus bundles}, which present exponential
distortion through cycling in a nicely geometric way.
  One of our goals is to bring out mathematical structure related to cuts and
cut elimination. Our geometry on groups through proofs is far from the word
metric precisely because of the cut rule. We want to explore the idea that in
general the existence of short proofs with cuts should be related to internal
symmetry or dynamical processes in the underlying mathematical objects.
  We also want to bring ordinary mathematical proofs closer to proof theory. In
this regard the topological example is attractive for presenting realistic
difficulties.
