A prospective comparison of research campaigns [ftip-00NU]
✍️source

    The purpose of the first experiment is to determine whether a developed mathematical contribution improves affordable retained capability in § [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.

    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.

    1. An exact classical solver constructs certificates by elimination and decomposition, including all certificate production and checking.
    2. A fixed initial agent uses direct attempts and verification feedback, establishing the reference capability under the common deployment cap.
    3. 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.
    4. The same recipient acquires a contribution from the specified developmental producer, with producer preparation, validation and teaching included in the campaign resources.
    5. 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.

    AlphaEvolve motivates allowing invented algorithms and code; TTT-Discover motivates updates during search; ThetaEvolve motivates frozen transfer. Nexus and OEIS Open 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 First Proof; longer campaigns can use archives and communication as in Station. Problem selection can also be assessed prospectively, following the question posed by FAR. 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.