Why Mathematical Problems Are Hard for Agents in Practice

Introduction

I have been following the progress of AI in mathematical research for some time, reading research papers, Agent-system reports, and public review records along the way.

This article is an interim attempt to organize what I have learned. Through concrete cases, it tries to clarify some of the current difficulties at the intersection of mathematical research and AI, although the picture is certainly not yet complete.

The discussion follows four kinds of difficulty: strategic uncertainty, interdependent technical problems, error accumulation in long proofs, and preservation of useful information from failed attempts. Drawing on system implementations and expert reviews, I focus on how these problems arise and why they are difficult to resolve.

1. Strategic uncertainty

The first difficulty in mathematical research is not knowing which proof strategy to choose. A subtler problem is that a system may find an apparently complete route without being able to tell whether that route has actually made the problem easier.

1.1 Naming the core difficulty a “lemma” does not solve it

Consider Problem 3 from the second First Proof evaluation batch. Submission C reduced the problem to two key lemmas. The review noted that the cited literature contained neither result; even a weakened form of one lemma would imply a form of the Csóka conjecture that was unresolved at the time of review. The downstream reduction was largely reasonable, but the central difficulty remained untouched.

This kind of failure can be abstracted as:

If lemma L holds, then target theorem T holds.

An Agent proves this implication and adds “prove (L)” to its task list, as if most of the work were complete. But (L) may be just as hard as the original problem—or stronger and harder.

A reduction can, of course, be valuable. Turning an unfamiliar problem into one with a clear structure and mature tools is itself progress.

From an Agent-execution perspective, however, this is particularly risky. Suppose a planner creates ten subtasks. Nine are easy, while the last contains nearly all the originality. A “90% completion rate” says almost nothing about the true mathematical progress.

1.2 Repeated revision may only circle within the same incomplete framework

The Momus paper analyzes an existing solver-verifier workflow. On PB-Adv-011, the system classified only the injective solutions, did not rule out non-injective solutions, and explicitly acknowledged the gap—yet its internal verifier approved the answer five times in a row.

If the generator keeps rewriting the argument while the verifier keeps checking the already-correct local results, the system may appear increasingly stable without getting any closer to a complete answer.

This case comes from competition-style proof tasks and cannot directly establish success rates for open mathematical research. It does, however, expose a mechanism worth guarding against: more iterations do not necessarily push a system outside its original frame of thought.

2. Distributed dependencies

Mathematical problems can be decomposed, but after decomposition the parts must connect with complete precision.

That connection involves more than “run task B after task A.” It includes the ambient space of each object, permitted assumptions, parameter ranges, quantifier order, and whether an upstream result is valid under the conditions required downstream.

2.1 The rational version is done, but the integer version is not

One Danus research case concerns the construction of tangent classes of matroids. The system first completed a rational-coefficient version, while the original task required an integer-coefficient version. The accompanying paper explains that the problem used the same notation for an integer object and its rationalization, and this notational omission contributed to the misunderstanding. Only after a human pointed out the distinction did the system complete the integer version.

This case directly reveals a problem of task understanding and objective alignment. In multi-Agent collaboration, the same ambiguity can occur at handoffs: an upstream Agent believes it supplied the required object; a downstream Agent assumes the object satisfies a stronger condition; and the final synthesizer sees an argument that looks complete on the surface.

Similar distinctions include “finite-dimensional” versus “arbitrary-dimensional,” and “for every parameter there exists a constant” versus “there exists one constant for all parameters.” The phrases look close, but their mathematical meanings differ.

2.2 The dependency graph is rarely complete at the start

A LeanMarathon formalization case reveals another difficulty. While formalizing a proof related to Erdős Problem #1196, the system traced a seemingly straightforward estimate down to monotonicity of the Dirichlet eta function, then to stochastic-order comparisons of Gamma distributions and a Mellin representation.

A short subsection does not imply little mathematical dependence. A paper's phrase “by standard methods” may invoke an entire body of assumed knowledge. For a formalization Agent, that knowledge must become callable theorems or be proved again.

The initial task “prove estimate A” may therefore become: A depends on B; B depends on C and D; C requires a distribution comparison; and D requires an integral representation together with its conditions of applicability.

This is not merely adding steps to the original task. Execution reveals that the initially understood task boundary was inaccurate.

Moreover, a single proof route often requires several lemmas to hold simultaneously, while different routes may substitute for one another. When a node fails, the system may need to decompose it further, revise an upstream statement, or abandon the entire route.

This also explains why “local rework” is not just another model call. If a system adds an assumption to prove a lemma, every downstream step depending on that lemma must be checked again to ensure that it satisfies the new assumption.

3. Long proofs

As an argument grows, a system must continuously preserve consistent definitions, complete assumptions, valid dependencies, and the relationship between local conclusions and the global objective.

3.1 Simple local rules do not make global properties easy to prove

The Knuth cycles case asks for all edges of a class of directed graphs to be partitioned into three Hamiltonian cycles. The paper reports that one construction passed computational checks for (m\leq 2000), and that two constructions produced proof drafts of 46 and 75 pages respectively. The central challenge is to prove that short local routing rules yield the target cycles at every relevant size, rather than several shorter cycles.

A simple example illustrates the difference.

Suppose every vertex in a finite directed graph has exactly one incoming edge and one outgoing edge. This local condition does not guarantee that every vertex lies on a single cycle. The graph may instead consist of two disjoint cycles.

“Every local rule is valid” and “the complete construction has the target property” are therefore distinct proof obligations. Local checks cannot replace a missing global argument, and finite computational experiments cannot directly replace a proof for all sizes.

3.2 Turning accepted facts into a paper can introduce new errors

The Danus team reports that reorganizing and compressing accepted facts into a readable paper can still introduce errors.

The reason is straightforward. Turning several existing facts into a fluent narrative often requires connective claims such as:

“Therefore, the two operations can be exchanged.”

“The result also applies to the boundary case.”

“Without loss of generality, we may fix a parameter.”

These sentences look editorial, but each may contain a new mathematical assertion. If the accepted results do not cover it, a new proof obligation has appeared.

Preserving a complete derivation and generating a readable proof are thus related but different tasks. The former emphasizes retaining information; the latter emphasizes compression, reorganization, and explanation. The more aggressively an argument is compressed, the more carefully the system must check which premises were omitted and which connections were assumed.

Literature citation is a similar cross-document dependency. The Aletheia research report says that tool-use training and retrieval reduced fabricated paper titles and authors, yet another error remained: the paper was real, but the claimed result was not in it.

3.3 Passing formal verification still requires checking that the original proposition was verified

A case study of autonomous research collectives records an even more direct form of objective drift. In the authors' research simulation, some Agents used local notation to shadow mathematical predicates, causing the original problem to be interpreted as an easier proposition. The code compiled in Lean but did not prove the original mathematical problem; after it entered the shared library, other Agents imitated it.

The surrounding system failed to reliably preserve consistency between “the proposition requested” and “the proposition actually sent to the checker.”

Two questions must be distinguished:

Whether a formal proposition was proved correctly and whether that proposition faithfully expresses the original problem are not the same check.

4. Failed attempts

Failure in mathematical exploration is not a single kind of event.

Failing to find a proof, finding a counterexample, proving a special case, and discovering that an extra assumption is indispensable all carry different information. Compressing them all into “failure” discards exactly what the next research cycle may need.

4.1 A rejected proof may contain reusable results

Submission B for First Proof Problem 3 was rejected because its central comparison lemma had a counterexample. The review nevertheless confirmed that it correctly handled (p=1/2) and (p=1), and correctly excluded parameters outside ([0,1/3]\cup{1/2,1}). An incomplete proof does not make every result inside it invalid.

This case shows that failure should be handled more precisely than “retry” or “abandon.”

Suppose a proof route depends on lemma (L), and (L) turns out to be false. We can conclude that the argument depending on (L) cannot continue, but not that the target theorem (T) is false.

At the same time, local results independent of (L) may remain valid. Even when a general statement fails, a version for a special parameter range or with an additional condition may already have been proved.

This is mathematical information extraction, not ordinary summarization of a chat history.

4.2 Search failure is not mathematical refutation

Three superficially similar states require special care.

“No proof was found within the current budget” says only that this search did not succeed.

“A construction failed in computational experiments” says that this construction did not work on the tested instances, but it need not rule out other constructions.

Only “there exists a counterexample satisfying every assumption but violating the conclusion” refutes the corresponding proposition.

If an Agent records the first state as the third, the next cycle may wrongly abandon a valid route. Conversely, if a rigorous counterexample is reduced to “there may be a problem here,” later Agents may waste substantial effort on the same dead end.

5. Closing thoughts

Looking across Math Agent projects such as Momus, Aletheia, LeanMarathon, and Danus, a common principle emerges: do not treat mathematical research as a one-shot answer-generation task; organize it as a process that can continuously revise, verify, and track dependencies.

But having a fact graph does not make every fact correct. Having a verifier does not prevent the verification target from drifting. Saving failure records does not mean they accurately express the mathematical meaning of each failure. The value of an architecture must ultimately be judged by whether it protects these concrete boundaries.

The central challenge of mathematical problems in Agent practice is not merely generating new reasoning. It is accurately maintaining the boundaries among “proved,” “conditionally true,” “still unproved,” and “refuted” throughout an ongoing process of exploration, decomposition, revision, and forgetting.