符号非正式化的潜力
符号非正式化能够将形式数学可靠地转换为自然语言，具有人机可读性而不损失精确性。这一方法在传统证明系统中，将有限的语法糖机制推广至数学的普通语言。
人工智能与自动形式化的结合
在人工智能构建证明和自动形式化的场景下，符号非正式化可以清晰地解释所构建内容的具体含义。
Informath 项目
本文介绍了项目 Informath，旨在展示符号非正式化如何以合理的开发努力生成流畅的文本，并支持多种形式及自然语言。Informath 基于一种跨语言架构，其中 Dedukti 作为不同证明系统（如 Agda、Lean、Rocq）之间的中心，而语法框架（Grammatical Framework, GF）则负责不同自然语言的语言正确性和变异性。
博主点评： 符号非正式化的研究为形式化数学的可读性提供了新的视角，尤其是在人工智能辅助证明的背景下。这一领域的进展可能会极大地促进数学知识的传播与应用，值得关注。