据我所知

(a) 将数学定理和证明从英语转换为形式逻辑对于具有足够背景的数学家来说是一项简单的工作，只是需要时间。

(b) 一旦转换为形式逻辑，证明的计算机验证就变得简单了。

如果我们可以自动化 (a)，则在 (b) 已发表的研究论文上执行 (b) 可以节省大量时间和智力劳动（可以专门用于其他地方）。

请注意，如果整体求解 (a) 很困难，我们可以期望数学家能够半途而废地遇到计算机系统，并避免编写难以转换的冗长的英语段落。如果它变得足够可行，提交论文的正式逻辑版本甚至可以成为预期的标准程序。

解决 (a) 的额外好处是反向执行该过程：数学家可以将较小的任务和引理（琐碎和非琐碎的任务）委托给自动定理证明器 (ATP)。辅助定理证明将变得更加流行并提高生产力，甚至有时会通过提出论文作者无法提供的证明来让我们感到惊讶。如果我们预测未来 ATP 能力的急剧上升轨迹，这将更有价值。如果有的话，这可能是自我实现的，因为通过大量证明和正式逻辑格式的问题结合起来展示良好 ATP 的潜力可能会推动对 ATP 的研究增加。

如果我听起来像推销员，请原谅我，但这有多可行？在开发基于 NLP 的 AI 来转换论文时将面临哪些主要挑战？考虑到当今该领域的现状，这些挑战有多容易处理？

Ps 我知道 ATP 生成的证明通常很难直观地理解，并且最终可能会在没有明确暴露所使用的基础证明方法的情况下证明结果。但是能够使用最终结果仍然是一个好处