目前人工智能形式化证明数学定理遇到了哪些困难？有哪些最新进展？
数学定理的机器证明从古至今一直是数学家和计算机学家们的理想。数学的重大突破可以直接推动物理学甚至前沿科技的快速发展。人工智能若能证明极其困难的未解决的数学定理，也意味着将会超越人类，迈入通用人工智能。 根据数理逻辑，任何数学定理、命题、对象，都可以形式化为基本逻辑符号的排列组合，如定理“1 + 2 = 3”可以写为 1 加 “1 的后继”等于“1 的后继的后继”；定义了加法后可以定义乘法；可以用下面的逻辑链条表示定理“质数有无限多个”：对任意不能分解为除了1和它本身以外的乘积的数，存在一个比它大的数，不能分解为除了1和它本身以外的乘积。 在通常的自然语言处理中，词向量空间通常非常大，然而如果限定在逻辑词和已有的定理与名词上，则可以大幅度缩小该空间到几个基本的逻辑词。如果用形式化验证推理逻辑，则完全没有大语言模型的幻觉问题。可能可以通过监督学习的方式，让模型先学会人类已有的部分定理。可能可以使用强化学习，动作空间也不大。不过什么定理是“值得证明的”是个问题，比如“1 + 100 = 101”必然不是值得证明的定理，可能可以用已有的大语言模型辅助判断。由于精确定义含义，因此可能不用注意力机制相关架构。 目前这方面的研究有哪些进展？遇到了哪些困难？国内外有哪些团队正在进行相关的学术研究？