Extending the Informalization of Mathematics to Homotopy Type Theory

Abstract

The informalization of mathematics, i.e., turning formal mathematical expressions into informal natural language, is a developing area of study. Probabilistic approaches based on large language models have been used in earlier works to accomplish this task. Informath is an ongoing project to enable deterministic translation between formal and informal mathematics in multiple languages. It is built on Grammatical Framework and formalized Dedukti theory. It has not been demonstrated how this approach generalizes to advanced mathematics. We show how Informath can generate informal representations of the mathematics of Homotopy Type Theory. This is done by formalizing the book Introduction to Homotopy Type Theory by Egbert Rijke and extending the grammar to enable generation of informal expressions. We found that, while the theory could be formalized and informalized, there exist trade-offs between a natural formalization and the formalization that would produce the most accurate informalization to match the original expressions in the book. These trade-offs arise when the formal representation lacks a direct correspondence to the original informal expression. Different approaches were tested to match existing formalization and align with the informal base. The results indicate that Informath is able to informalize Homotopy Type Theory, but the structure of the formalization may need to be structured around the desired result to get a matching informalization.