Computer support for document interaction is only possible if some aspects of the meaning of the document content are made explicit - i.e. formalized and dealt with with formal methods. In many cases, useful mathematical services can be rendered by machines without having an entailment relation, for instance we can search for a formula, we can determine the concepts it depends upon, etc. The commonality of such services is that they are based on the structure of the formulae alone. For instance, instead of relying on a formal calculus to determine theorem-hood, we only insist that there be an object that has the structure of a proof. We speak of structural semantics as a lightweight form of meaning annotation.

So instead of formalizing mathematical knowledge to a level where an entailment relation can be induced, we can use structural descriptions instead, e.g. by annotating certain properties to mathematical documents turning them into objects of flexible formality.