Any act of problem-solving combines prior knowledge, local search, and a third element that is less often discussed: the extraction of information from search to update understanding. I propose a model of mathematical problem-solving as a belief-update loop in which the mathematician generates auxiliary questions, resolves them through computation, and uses the outcomes to shift confidence in conjectures. The information yield of this loop depends on the vocabulary available to the solver, and I distinguish two forms of concept that reshape this vocabulary: implicit concepts, which improve pruning within a fixed language of moves, and explicit concepts, which introduce new moves that were previously inexpressible. I argue that explicit concept creation is the characteristic step of mathematical discovery, driven by necessity when no computation in the existing vocabulary can resolve the problem, and yielding shareability and composability as byproducts. Current AI systems, including those that achieve superhuman performance in games and formal theorem proving, operate exclusively through implicit concept formation. I discuss what it would take for machines to create explicit concepts, and consider how differing computational tradeoffs between humans and machines may lead to fundamentally different styles of mathematics.

翻译：任何解题行为都结合了先验知识、局部搜索以及第三个较少被讨论的要素：从搜索中提取信息以更新认知。本文提出一个将数学问题解决建模为信念更新循环的模型：数学家生成辅助问题，通过计算解决它们，并利用结果调整对猜想的置信度。该循环的信息产出取决于求解者可用的词汇表，我区分了重塑该词汇表的两种概念形式：隐式概念——在固定的操作语言中改进剪枝效率；显式概念——引入先前无法表达的新操作。我认为显式概念的创造是数学发现的标志性步骤，当现有词汇表中的任何计算都无法解决问题时，这一步骤由必要性驱动，并产生可共享性与可组合性作为副产品。当前的人工智能系统（包括在游戏和形式化定理证明中实现超人类性能的系统）完全通过隐式概念形成运作。我将探讨机器创造显式概念所需的条件，并思考人类与机器之间不同的计算权衡如何可能导致根本不同的数学风格。