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