这篇论文介绍了一个叫Informath的项目，能把数学证明自动转成自然语言，支持多语言和多个证明系统（Agda、Lean、Rocq），对形式化验证和AI可解释性很有用。
这篇论文提出Informath项目，基于Dedukti作为不同证明系统（Agda、Lean、Rocq）之间的枢纽，并利用Grammatical Framework（GF）处理多语言语法正确性。符号非形式化将形式化数学可靠地转换为自然语言，使机器验证的内容可读。论文展示了Informath能以合理的开发成本生成流畅文本，并支持多种形式语言和自然语言。
Symbolic Informalization: Fluent, Productive, Multilingual
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.