 An alternative picture is that the formal and informal languages offer different ways of expressing mathematical theorems and proofs. The formal language is not used to ‘translate’, and hence does not need to be measured against what is expressed in an informal proof. Rather it offers its own, arguably superior, resources for expressing the content of mathematical statements in a precise and rigorous setting that has been specifically designed for this purpose. Whichever picture is adopted of the relation between formal and informal presentations of mathematics, two points remain. First, deductive mathematical arguments—arguments that are produced, transmitted, and built upon by mathematicians—can be either formal or informal. Second, the evaluation of such arguments as being deductively valid or invalid is easier to carry out definitively in the context of a formal system of some sort.