Symbolic Informalization: Fluent, Productive, Multilingual
For mathematicians and AI researchers, this provides a method to make formal proofs accessible without precision loss, though it is an incremental extension of existing syntactic sugar and autoformalization ideas.
The paper introduces symbolic informalization to convert formal mathematics into fluent natural language, enabling human-readable machine-checked content. The Informath project demonstrates this with an interlingual architecture connecting proof systems (Agda, Lean, Rocq) via Dedukti and using Grammatical Framework for multilingual output.
Symbolic informalization enables a reliable conversion of formal mathematics to natural language. It has the potential to make machine-checked content human-readable without loss of precision. In a traditional proof system usage, symbolic informalization generalizes the limited mechanisms of syntactic sugar into the ordinary language of mathematics. In a setting where proofs are constructed by artificial intelligence and autoformalization, symbolic informalization can explain what precisely has been constructed. This paper outlines the project Informath, which aims to show how symbolic informalization can produce fluent text with a reasonable development effort and address multiple formal and natural languages. Informath is based on an interlingual architecture, where Dedukti works as a hub between different proof systems (Agda, Lean, Rocq) and Grammatical Framework (GF) takes care of linguistic correctness and variation in different natural languages.