Why is proving theorems so hard for machines, and what would an AI need for automated mathematical discovery rather than just solving exercises? A 2026 arXiv essay by Maissam Barkeshli, Michael Douglas and Michael Freedman gives a precise answer: the space of provable statements explodes so fast that only heavy compression, in the form of abstraction, makes human mathematics reachable at all. The piece is a preprint and an explicitly speculative research program, not a set of experimental results.

What follows walks through its main ideas, the numbers it uses to make them concrete, and the limits the authors themselves state. The common thread is what it would take for a program to find the important parts of mathematics on its own.

The setting: AI is already good at some mathematics

The essay, “Artificial Intelligence and the Structure of Mathematics,” was submitted to arXiv on 7 April 2026. It opens by listing recent results, as the authors describe them: gold-level performance on the 2025 International Mathematical Olympiad, saturation of Putnam-level problem sets, solutions to many top-tier FrontierMath problems, and AI agents helping to complete formal proofs of the prime number theorem and of higher-dimensional sphere packing in the Lean proof assistant.

Their aim is not to add to that list. They ask a structural question. Of all the statements that could be proved from a given set of axioms, only a tiny portion is what people call mathematics. Could an autonomous agent, like a space probe sent into an unexplored landscape, find that portion and report back what matters? The authors say plainly that they want to show these questions can be studied precisely, not to answer them.

Mathematics as a graph of proofs

The framework starts with the universal hypergraph, written U. Its nodes are provable propositions. Its directed, ordered, colored hyperedges are deductive rules, and the axioms are the roots. The construction follows dependent type theory, the foundation of proof assistants such as Lean and Coq. A companion structure, the structural hypergraph S, includes every expression, not only propositions, so it can hold functions, data types and abstractions.

A key bridge is the Curry-Howard correspondence, which says a proof is itself an object that can be placed in a graph. In the essay, U is the “shadow” of the graph of proof objects, P.

Different foundations give different graphs. Peano arithmetic, ZF and ZFC each define one, and Gödel’s incompleteness results guarantee that some statements are independent of any given system. Two systems can prove the same statements while the shape of their proofs differs, and the authors note that some results about which statements hold across systems depend on procedures that are not even computable. So the large-scale geometry of mathematics may depend on its foundations.

The explosion, in numbers

The size of U is the first obstacle. The essay argues it grows at least doubly exponentially with depth. In a toy propositional example with k initial propositions, the count after j steps is k raised to the power 2^j. Even with two starting statements, ten steps gives 2 to the 1,024th power.

Proof search faces a related wall. If each step offers about b choices and the proof needs depth D, brute-force search takes time on the order of b^D. The essay lists three standard ways to cut it down.

Technique Search time
Plain search About b^D
Meet in the middle (search from both ends) About 2b^(D/2)
Hierarchical planning (as the authors model it) About C b^(D/10)
Linear deductions with a fixed library Singly rather than doubly exponential

Each helps and none removes the exponential. Their estimate for the hardest proof a machine can find follows a simple form: the maximum complexity it can reach grows with the logarithm of available time. In practice, that is a slow climb. Ten times more computing buys only a modest increase in proof complexity.

Why abstraction is the way out

Humans do not search this space blindly. They invent definitions and lemmas that package long chains of reasoning into a single named step. The essay treats abstraction as the central compression mechanism. A good abstraction shortens proofs, but it also adds to the set of available moves, so the branching factor grows. Finding an abstraction of size c(A) takes time roughly proportional to the corpus size times b_eff to the power c(A), which caps how big a new idea the agent can discover at once.

The payoff can be dramatic, and the paper gives a striking illustration. It cites the longest proof in Lean’s Mathlib library (as of 17 October 2025), which runs to about 600 lines but expands to something on the order of 10 to the 104th power when written out as a tree in the most basic terms of Lean 4. Nested definitions compress that enormously. The authors make a conjecture-flavored claim on this basis: the full space U admits only polynomial compression, while human mathematics H admits broad exponential compression. They rest this on their earlier work and flag it as such, so it counts as a hypothesis for now.

Human mathematics as a thin ribbon

If that is right, human mathematics is not a random patch of U. The authors cite evidence from that earlier work that H grows only polynomially, and describe it as a “ribbon” running through a space that expands doubly exponentially. The practical meaning: the thing that makes mathematics learnable by people may be the same thing a machine must exploit.

The essay proposes ways to measure which results are worth finding. One is efficiency, E(P), the ratio between the minimal total complexity of a proof and the length of its shortest expression. Another is whether a node is a hub with many outgoing edges or a bottleneck that links clusters, as in the proof of Fermat’s Last Theorem. The authors add a metaphor of a willow tree: theorems are low-hanging leaves on tall branches. They also admit that “interestingness” depends on history and human preference, and that connectivity is hard to define since each node has infinitely many connections.

What a discovery agent would have to do

The essay frames an agent as a reinforcement-learning system whose state is a growing corpus of mathematical objects and whose actions add or remove nodes. The immediate trouble, the authors note, is that mathematics has no clear intrinsic objective function. They outline a generic loop: generate a goal, attempt it, learn and abstract from the result, then curate and compress the corpus.

Conjecturing is treated as a separate skill. It can use deliberately unsound rules, such as inferring B implies A from A implies B, and inductive generalization from examples. The paper even asks whether one could do mathematics without conjectures.

The authors survey existing systems as proofs of principle: deductive tools such as IsaCoSy and Minimo, inductive conjecture generators in the Graffiti family, program-synthesis systems such as DreamCoder, and constructive search systems such as FunSearch and AlphaEvolve. They see these as showing that automated discovery is possible in small domains. The acid test they name as not yet achieved is sustained discovery in a closed loop, with the system generating and curating its own goals.

What the essay does not claim

This is a framing document. Much of the framework is speculative and offered as a research program. The complexity measures are uncomputable over all of U and can only be calculated on finite truncations. Several load-bearing claims, including the compression dichotomy and the polynomial growth of human mathematics, come from the authors’ earlier work rather than from experiments in this paper. Only the first part of the paper could be read in full for this write-up; the sections on human mathematics and the proposed criteria for discovery agents were not reviewed here.

Why read it anyway? Because it supplies vocabulary that is missing from most coverage of AI and mathematics. Benchmarks measure whether a model can solve a problem someone else posed. This essay asks what it would mean for a system to decide for itself what is worth proving, and offers measurable proxies for that question.

How this differs from benchmark progress

A benchmark gives the model a question with a known answer. Discovery turns that around: the system has to choose its own questions, decide which of its results deserve to be kept, and fold them into a library that shapes later searches. Two systems with the same score on a problem set could differ completely on this axis. One might be a strong solver that never improves its own toolkit, and the other might be a modest solver that builds better abstractions each round.

The essay’s compression argument suggests why the second kind matters. If the reachable proof complexity rises only with the logarithm of compute, then waiting for raw speed to deliver new mathematics is a slow bet. Better abstractions change the exponent instead of the clock, which is why the authors spend so much of the paper on how to represent, score and reuse them.

What to watch

  • Whether the compressibility claim for human mathematics holds up when others test it on different libraries of formal proofs.
  • Whether any system closes the loop the authors describe, setting its own goals and abstracting from the results.
  • Whether proxies such as the efficiency ratio E(P) track what working mathematicians call deep or useful.

Sources