# Strongest Counterargument — We Are Not Running Out of Problems

Status: `PRE-DRAFT STEELMAN / REQUIRED BEFORE ARTICLE PROSE`

## The counterargument

The apparent story is that AI has begun consuming a finite backlog of
human-formulated mathematical problems. The stronger interpretation of the
available evidence is almost the opposite:

> We are not observing the depletion of a mathematical frontier. We are
> observing a new proof-production system operating on a small, unusually
> machine-readable selection of problems, while the definitions of problem,
> solution, novelty, difficulty and replenishment remain unstable.

Eight retained AlphaProof Nexus results are real evidence of capability. They
are not yet evidence of exhaustion, acceleration or even a declining stock.

## 1. The denominator is an experiment, not a frontier

The strongest denominator in the workpack is 353 attempted formalized Erdős
records. It measures one selected experiment. It does not measure all open
Erdős problems, all formalized research mathematics or all human-formulated
mathematical questions.

The cohort is conditioned on having a usable formal statement and fitting the
system's run design. That selection may favour problems whose conceptual work
has already been compressed into a proof-assistant target. A success ratio
inside that cohort is informative about the system and the cohort. It cannot
be promoted into a depletion percentage for mathematics.

## 2. Solving a problem does not subtract one fixed unit

Mathematical problems are not identical tokens in a warehouse. A resolution
can:

- create stronger variants;
- expose the real obstruction;
- split one question into several better questions;
- introduce a reusable construction;
- reveal a formalization error;
- revive an ignored literature connection; or
- change what experts consider the important problem.

Problem 741(i) split under audit into natural-, upper- and lower-density
interpretations. Problem 138 contains several distinct questions. Problem 26's
counted variant does not inherit the identity or age of the root problem.
Resolution can increase the visible frontier rather than merely reduce it.

## 3. The audit found bookkeeping progress as often as frontier consumption

The nine reported Erdős artifacts became eight strict-core events only after
individual review. Erdős 846 is mathematically correct and independently
generated, but a 2024 theorem already implied the answer. Other rows required
statement clarification, variant boundaries, corrected dates or separation of
formal and prose constructions.

This suggests that part of the apparent acceleration may be an acceleration in
discovering what was already provable, what had been ambiguously stated and
what had not yet been connected across literatures. That is valuable. It is
not the same phenomenon as machines consuming an untouched frontier.

## 4. Formalized inputs contain substantial human work

A formal target is not a raw question. Humans have selected the problem,
translated it into a formal language, chosen definitions, imported libraries,
encoded known mathematical infrastructure and decided what counts as a proof
of the target.

The agent may still supply the decisive construction and complete proof. But
the experiment does not measure the cost of creating the formal environment or
the failures that occurred before a successful target was ready. Calling the
result autonomous without pricing that infrastructure risks confusing the
last visible step with the whole research process.

## 5. Public success artifacts are not a throughput series

The corrected public dates place two retained events in Q1 and six in Q2 2026.
That does not establish acceleration. They come from one system, one research
program and one clustered disclosure period. The apparent quarterly rise can
be caused by publication timing, batching, selection or artifact release.

There is no comparable earlier run, later accepted snapshot, stable compute
budget or complete failure log. A curve fitted to two adjacent quarters would
model the disclosure process at least as much as the solving process.

## 6. Replenishment is not counted

The depletion thesis requires two flows:

- verified resolutions leaving a defined stock; and
- comparable new problems entering it.

Only the first has a partial experimental count. No accepted rule currently
decides when a new conjecture, variant, generalization or formalized question
is comparable in depth to a resolved problem. Without that rule, the claim
that AI resolves problems faster than humans replenish them has no measured
right-hand side.

The human frontier may expand faster precisely because machines lower the cost
of exploring consequences and generating sharper questions.

## 7. Difficulty is not measured by age

Problem age is useful context, not a calibrated difficulty scale. A 56-year-old
subproblem may persist because it is obscure, ambiguously stated or low
priority. A new problem may be structurally much harder. Formalization can also
make an old problem unusually tractable without making the underlying field
easy.

The current median known age of 32 years cannot show that AI is moving toward
deeper mathematics. The pack has no independent difficulty score, prestige
control cohort or expert ranking.

## 8. Formal correctness is not evidence that humans have lost understanding

The workpack raises the possibility that machine proofs may outrun human
conceptual comprehension. It does not measure that possibility.

Several PDFs simplify or diverge from the Lean proofs. In 846, the prose omits
the hardest case analysis. That may indicate an exposition gap, but it does not
show that mathematicians cannot understand the construction. Humans publicly
interpreted, corrected and generalized several of the results. The available
evidence may instead show a new division of labour: machines close formal
details while humans identify meaning, scope and connections.

## 9. Literature grounding remains a central weakness

Erdős 846 is the clearest warning. Two models independently found elegant
proofs, while a human expert recognized that prior work already implied the
answer. This is not merely a database clerical issue. Novel mathematical
research depends on knowing when a result already exists in another language,
setting or theorem family.

Until literature retrieval and priority review are integrated into the same
workflow, proof generation can outrun novelty verification. The number of
formally accepted results can rise without an equal rise in new mathematics.

## 10. The visible sample is shaped by reporting incentives

Successful formal proofs are easy to publish and count. Failed runs, abandoned
targets, expensive searches, human repairs and negative evaluations are less
visible. Company and laboratory result repositories are curated outputs, not
complete experimental logs.

The OEIS line demonstrates the problem directly: the paper reports 44
successes, while public artifacts currently reconstruct only 38 target files
representing 37 unique sequence IDs. Even the numerator is not yet a stable
public object.

## 11. Capability growth would still not imply exhaustion

Suppose future systems do show a rapidly rising verified resolution rate. The
depletion conclusion would still require additional premises:

- a fixed or slowly growing problem stock;
- comparable problem units;
- no compensating increase in new conjectures;
- no shift toward harder newly visible questions;
- sustained validation capacity; and
- a reason to treat unformulated mathematical territory as irrelevant.

None follows automatically from proof throughput. Faster telescopes did not
make astronomy run out of sky. Faster proof systems may change the boundary of
what humans can ask and inspect rather than empty it.

## Strongest conclusion against the thesis

The current baseline is better interpreted as evidence for a transition in
mathematical workflow:

> Machines are becoming capable proof partners inside carefully prepared
> formal environments. The immediate bottleneck may move from proving to
> choosing, formalizing, interpreting, connecting and validating questions.
> That is a major change in mathematics, but it is not evidence that the stock
> of meaningful problems is running out.

## What would weaken this counterargument

The counterargument should be revised if future evidence supplies all of the
following:

1. multiple accepted snapshots under stable inclusion rules;
2. at least twenty individually audited, independently validated full
   resolutions across more than one system and problem family;
3. complete attempted and failed-run denominators;
4. compute-normalized resolution rates;
5. a defensible, versioned replenishment measure;
6. evidence that solved-problem difficulty is stable or increasing;
7. systematic literature-priority checks with a low rediscovery rate; and
8. expert evidence that explanation and conceptual integration are falling
   behind verified proof production.

Until then, the depletion thesis remains an interesting scenario rather than
an empirical finding.

## Editorial use

Any later article must let this argument survive in full. It cannot be reduced
to a paragraph saying “of course mathematics creates new questions.” The
counterargument attacks the unit, denominator, chronology, novelty, autonomy,
difficulty proxy, replenishment measure and interpretation of the evidence.

If the article cannot answer those objections with data, its honest answer is:

> We do not yet know whether the curve is bending, because we do not yet have a
> curve.