![自动将以 .tex 编写的数学公式转换为保留所有数学信息的规范形式](https://linux22.com/image/387850/%E8%87%AA%E5%8A%A8%E5%B0%86%E4%BB%A5%20.tex%20%E7%BC%96%E5%86%99%E7%9A%84%E6%95%B0%E5%AD%A6%E5%85%AC%E5%BC%8F%E8%BD%AC%E6%8D%A2%E4%B8%BA%E4%BF%9D%E7%95%99%E6%89%80%E6%9C%89%E6%95%B0%E5%AD%A6%E4%BF%A1%E6%81%AF%E7%9A%84%E8%A7%84%E8%8C%83%E5%BD%A2%E5%BC%8F.png)
我相信我将要描述的事情能够准确完成。但我不确定这有多难。
基本上,我的动机是将大多数现有数学论文中的数学部分标准化,以便它们可以被搜索并输入到未来的自动定理证明器中。由于通过机器学习完全准确地处理 PDF 是不可能的现在我们必须依赖 .tex 文件。为了准确地做到这一点,我们需要能够将用 .tex 编写的数学论文转换为使用 ASCII 字母编写的其他独特形式,即对于任何独特的数学符号,应该有且只有一个表示。LaTeX 本身不满足此条件,因为它保留了许多与数学无关的排版信息,例如是否应该在n\to\infty
下方或右侧,\lim
并且因为有很多用户定义的宏。
请问我需要知道什么才能开发出可以进行此类转换的工具?我是否需要修改 TeX 引擎,以便它生成数学的规范表示而不是 .dvi 或 .pdf 文件?