数学概念的机械化创建

任何问题解决行为都结合了先前知识、局部搜索以及一个较少被讨论的第三要素：从搜索中提取信息以更新理解。我提出将数学问题解决建模为信念更新循环的模型，其中数学家生成辅助问题，通过计算解决这些问题，并利用结果在关于猜想的置信度方面进行调整。该循环的信息产出取决于求解者可用的词汇，我区分了两种概念形式，以重塑这一词汇：隐式概念通过改进固定移动语言中的修剪来提升效率；显式概念则引入先前不可表达的新移动。我认为显式概念的创建是数学发现的特征性步骤，由必要性驱动——当现有词汇中没有计算能够解决问题时——并产生可分享性和可组合性作为副产品。当前的人工智能系统，包括在游戏和形式定理证明中实现超人类表现的系统，仅通过隐式概念形成运行。我讨论了机器如何创建显式概念，以及人类与机器之间不同计算权衡可能导致根本不同的数学风格。