The Agent as Mathematician: Proof, Verification, and Creation in an Algorithmic Agent

Knowing the rules of a game completely doesn't mean you can play it cheaply — and this paper makes that precise for mathematics.

The setup is an "algorithmic agent": a system that survives by maintaining a compressed model of its world and acting to keep that model accurate. The paper asks what such an agent is doing when it does mathematics. The answer: mathematics is just another world to model, with one twist — the agent wrote the laws itself. The axioms are the micro-laws, and everything they entail is fixed the moment they're written. Yet knowing the rules completely doesn't make the consequences accessible. This is the same obstruction that blocks deriving fluid dynamics from molecular physics: complete knowledge of the micro-rule, and the macro-structure still has to be discovered. Mathematics presents this in unusually pure form because there's no unknown initial condition to blame. The barrier is intrinsic to the deductive relation itself.

The paper carves mathematical activity into four distinct operations: positing a theory (choosing axioms and vocabulary), verifying a certificate (running a checker), searching for a certificate (proof discovery), and reorganizing the model through definitions and lemmas. These are genuinely different in kind. Verification is a hard-gated, mechanical action — a trusted subroutine that returns a binary verdict. Discovery is planning under a sparse objective, where the only unambiguous signal is a completed proof. Positing a theory is a meta-level modeling decision, not an inference within any theory, and it carries the deepest computational burden: choosing the right axioms and vocabulary is uncomputable in general, so it must be done empirically, by trying representations and keeping what works.

The paper's central positive claim separates two things that are easy to conflate: deductive content and computational accessibility. Adding a proven theorem as a lemma changes nothing about what a theory entails — the deductive closure is identical. But for a bounded agent, it can dramatically cut the cost of future proofs. This means the value of a mathematical library is entirely in access, not in new truth. The paper formalizes this as an amortized condition: a library of lemmas earns its construction cost exactly when reuse recovers it across a workload of later problems. Mathematical taste, on this account, is partly an empirical bet about which problems will arise.

This leads to the paper's "convenient representative" principle. Compression — finding the shortest description — is the right criterion for selecting which model-function to use. But it's the wrong criterion for selecting how to hold that model. The shortest program for a mathematical world is the bare axioms, which force you to re-derive everything from scratch. A bounded agent should instead hold a functionally equivalent but more "unwrapped" implementation, expanded to the grain of the questions it actually faces. The two criteria — compression for generalization, convenience for accessibility — operate at different levels and neither substitutes for the other.