我相信我将要描述的事情能够准确完成。但我不确定这有多难。
基本上，我的动机是将大多数现有数学论文中的数学部分标准化，以便它们可以被搜索并输入到未来的自动定理证明器中。由于通过机器学习完全准确地处理 PDF 是不可能的现在我们必须依赖 .tex 文件。为了准确地做到这一点，我们需要能够将用 .tex 编写的数学论文转换为使用 ASCII 字母编写的其他独特形式，即对于任何独特的数学符号，应该有且只有一个表示。LaTeX 本身不满足此条件，因为它保留了许多与数学无关的排版信息，例如是否应该在n\to\infty下方或右侧，\lim并且因为有很多用户定义的宏。
请问我需要知道什么才能开发出可以进行此类转换的工具？我是否需要修改 TeX 引擎，以便它生成数学的规范表示而不是 .dvi 或 .pdf 文件？