Mihnea Iancu

• The application of computer-based methods to mathematics, while meaningful, is constrained by the fact the most mathematical knowledge exists in forms that can only be understood by humans. In order for it to be also understood by machines, those aspects of mathematical knowledge that are relevant for machine-driven applications need to be made explicit. One important aspect of mathematics is the underlying semantics which can be made understandable to machines by formalizing it. Formalization makes explicit the implicit definitions and inference steps that occur naturally in mathematical documents. But, despite numerous attempts, only a small fragment of mathematics has been formalized because formalization is prohibitively expensive. Furthermore, existing formalized mathematics typically lacks in other aspects such as presentation information and narrative structure that are common in mathematics and critical for human-oriented practical applications. Therefore, existing applications for formal mathematics are mostly limited to verification so there is little practical incentive for formalization. Relying on the idea of flexiformality we propose flexiformalizing mathematics which addresses the bottlenecks discussed above in two ways. First, by allowing content of flexible formality, it minimizes the starting cost of flexiformalization compared to formalization. Second, by co-representing the narration, structure and meaning of mathematical knowledge it forms a basis for not only machine processing but also for building practical, human-oriented applications. We call the result of flexiformalization as described here flexiformal knowledge and we believe mathematical knowledge is fundamentally flexiformal.