Convention. A prospective comparison of research campaigns [ftip-00NU]
AGENTDRAFTED
The purpose of the first experiment is to determine whether a developed
mathematical contribution improves affordable retained capability in
Example [ftip-00NS]. The family, algorithm interfaces, model versions, seed
schedule, success threshold and resource profiles are fixed before the
contribution conditions are compared. A task initially easy for the agent
cannot demonstrate overcoming its initial difficulty; a task solved cheaply
by an admitted classical method cannot demonstrate a general discovery
barrier. Both are informative outcomes.
The assay convention for transfer, remix and construction makes these outcomes separately testable while preserving the fixed family, reveal schedule and resource controls below.
Information revealed by the generator, certificate interface, exposed
checker code or accessible literature belongs to the initial endowment.
If it supplies the homology formula, evaluate construction and reuse of a
certifying method rather than rediscovery of that formula.
A proposed pilot uses four disjoint sources of instances: admission
probes, development episodes, development validation and final evaluation.
Admission tests the initial agent without adaptation on 32 probes at a
fixed per-probe budget. An operational admission threshold is at most eight
accepted certificates. This threshold is a declared experimental choice,
not a theorem about the model. Report every admission result. If the chosen
family fails this condition, retain the result as an easy-family finding;
any revised family starts a new prospectively specified experiment. Do not
search for a family on which the assisted condition has already won.
One concrete size profile gives development objects at most eight
dimensions in each degree, with up to eight generating moves; final
in-distribution instances use the same profile and new seeds. A separate
extrapolation set permits dimensions and move counts up to sixteen.
For dimension cap \(d\), allow at most \(8d+16\) transformation steps
and \(64(d+1)^3\) binary matrix entries in a certificate; check dimensions,
indices and invertibility explicitly. All conditions share these limits,
and generation rejects instances whose retained certificates exceed them.
The pilot evaluates 128 final instances per regime, balanced between
positive and negative generation, across ten independent development seeds.
These are proposed settings, to be costed before execution; they are not
reported measurements.
Development validation may select a checkpoint, library or curriculum;
its repeated use and all discarded candidates are charged. Final instances
are revealed only after the retained artifact is frozen. A failed final
result cannot be used to revise that artifact within the same evaluation.
If another research generation uses those results, it receives a new final
set and a separate generation label. Exact repeated instances are excluded.
Fresh presentations with the same homology are intentional transfer tests,
not independent discoveries. For general-lemma assessments, screen equivalent
statements and trivial variable renamings across training and final sets.
The comparison includes the following complete procedures.
- An exact classical solver constructs certificates by elimination
and decomposition, including all certificate production and checking.
- A fixed initial agent uses direct attempts and verification feedback,
establishing the reference capability under the common deployment cap.
- An autonomous researcher develops lemmas, curricula, representations
and executable solvers from permitted initial material. Its search can
use experiments, counterexamples, retrieval, persistent archives and,
where the selected model permits it, parameter updates.
- The same recipient acquires a contribution from the specified
developmental producer, with producer preparation, validation and teaching
included in the campaign resources.
- Retrieval of existing mathematical methods is measured separately,
with the same declared library or literature access and charged search
and integration.
Within these conditions, compare relevant and irrelevant material at
similar context size, an acquired library with its removal, and a learned
curriculum with a predetermined curriculum. A parameter-acquisition claim
also compares against giving the same material in context without training.
These controls answer different questions and need not all share one
headline score. The stronger autonomous method may reconstruct the
contributor's development process, and that reconstruction is admitted
whenever its initial material and operations are available.
[novikov2025alphaevolve] motivates allowing
invented algorithms and code; [yuksekgonul2026testtime]
motivates updates during search; [wang2025thetaevolve]
motivates frozen transfer. [tsoukalas2026advancing]
and [adamczewski2026oeisopen] motivate comparing
richer research machinery against a strong simple loop. These choices
prevent the unaided condition from being defined as one deliberately weak
sampling recipe. They still form a finite tested collection, not every
admitted lineage in the theoretical conjecture.
The initial finite problem permits a later research extension. New
withheld lemmas can assess proof development in the manner of
[abouzaid2026firstproof]; longer campaigns can
use archives and communication as in
[chung2026autonomousdiscovery]. Problem selection can also
be assessed prospectively, following the question posed by
[zheng2026problem]. Such an extension receives its
own mathematical standard and evaluation schedule. Success on the finite
linear-algebra family does not establish success on research mathematics.