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.

翻译：符号非形式化实现了从形式化数学到自然语言的可靠转换，能够在保持精确性的前提下使机器可验证的内容具备人类可读性。在传统证明系统使用中，符号非形式化将语法糖的有限机制泛化为数学的常规语言。在由人工智能构建证明并通过自动形式化的场景下，符号非形式化能够精确解释所构建的内容。本文概述了Informath项目，旨在展示如何通过合理的开发投入，使符号非形式化生成流畅文本，并支持多种形式语言与自然语言。Informath基于中间语言架构，其中Dedukti作为不同证明系统（Agda、Lean、Rocq）之间的枢纽，而语法框架（GF）则负责不同自然语言的语法正确性与变体处理。