Faithfully Reflecting the Structure of Informal Mathematical Proofs into Formal Type Theories

Mathematical proofs, as written in every-day Common Mathematical Language (CML), are informal and many details are left implicit. To check such proofs with a proof assistant they need to be formalized and elaborated to full detail. In order to reduce the possibility of formalization errors and therefore increase the reliability of the translation of CML texts into type theories, we use a version of Nederpelt's formal language WTT extended with logical notation that encodes the natural deduction proof steps. By using this intermediate version, the subsequent translation into a full-fledged type theory can be made such that the proof clearly reflects the structure of the original CML proof. This makes it easier to ensure that the formalization of the CML text is done correctly, and offers additional advantages over usual representations of proof terms in type theory.