On the mechanical creation of mathematical concepts

TL;DR

This paper models mathematical problem-solving as a belief-update process involving auxiliary questions and concepts, highlighting the importance of explicit concept creation in discovery and contrasting human and AI approaches.

Contribution

It introduces a formal model of mathematical discovery emphasizing explicit concept creation and discusses implications for AI systems and human-machine differences.

Findings

Explicit concept creation drives mathematical discovery

Current AI systems rely mainly on implicit concepts

Explicit concepts enable shareability and composability

Abstract

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.