The current state-of-the-art in artificial intelligence is impressive,
especially in terms of mastery of language, but not so much in terms of
mathematical reasoning. What could be missing? Can we learn something useful
about that gap from how the brains of mathematicians go about their craft? This
essay builds on the idea that current deep learning mostly succeeds at system 1
abilities -- which correspond to our intuition and habitual behaviors -- but
still lacks something important regarding system 2 abilities -- which include
reasoning and robust uncertainty estimation. It takes an
information-theoretical posture to ask questions about what constitutes an
interesting mathematical statement, which could guide future work in crafting
an AI mathematician. The focus is not on proving a given theorem but on
discovering new and interesting conjectures. The central hypothesis is that a
desirable body of theorems better summarizes the set of all provable
statements, for example by having a small description length while at the same
time being close (in terms of number of derivation steps) to many provable
statements.

当前人工智能的最新技术在语言方面非常出色，但在数学推理方面则相对不足。本文以数学家的思维方式为参考，建立在当前深度学习在直觉和习惯性行为等方面取得成功的基础上，指出其在推理和稳健性不确定性估计等方面仍存在重要缺陷。文中以信息论的观点探讨了什么样的数学陈述是有趣的，这可能为塑造高级数学家人工智能的未来工作提供指导。重点不是证明给定的定理，而是发现新奇的猜想。核心假设是，一个有用的定理组应更好地总结所有可证陈述的集合，例如通过具有较小的描述长度，同时在推导步骤的数量上接近许多可证陈述。