Fix an initial agent, its available mathematical material and tools, a correctness standard, and a budget for an initial attempt. A problem is initially unresolved by this agent when the declared attempt procedure returns no accepted solution. A family-level measurement reports the initial success rate and its sampling uncertainty. Failure under this procedure neither proves that the solution is absent from pretrained weights nor establishes failure under every affordable procedure.

This operational condition permits three settings. In controlled rediscovery, evaluators know a useful mathematical concept and withhold its explicit construction. In withheld research problems, evaluators possess proofs that the agent cannot retrieve through its permitted interfaces. In open mathematical research, a result may also be new to the community. The initial agent can have relevant background knowledge in all three. Novelty, correctness and improvement over initial ability are different measurements.

The First Proof second batch provides a concrete withheld-research protocol: human-proved research lemmas were evaluated before their proofs were published, with organizer-run agents, a time limit and expert assessment. Its released statements and logs are now public, so a new experiment must use fresh withheld material or state which reconstruction of earlier access is being tested. An agent's accepted alternative proof can be a substantive discovery even if the theorem has an existing human proof.

The research campaign has three observable products. A discovery is an accepted mathematical result or method obtained during development. An acquired artifact is the state retained for subsequent work: parameters, a checked library, an executable representation, a search procedure, or an explicitly specified combination. Transfer is the performance of that frozen artifact on new problems under a common deployment budget. A successful answer to the current problem alone does not establish transfer. Continuing to consult the contributor during evaluation changes the system being measured and must be a separate condition.

DreamProver (sections 3--5) illustrates how research produces a reusable library. Failed training goals are decomposed into helper results; a later phase clusters, generalizes, verifies and prunes candidate lemmas. Libraries are then evaluated on separate theorems. The learned lemmas may be well-known mathematics, and the retained artifact is available in context rather than necessarily encoded by a parameter update. This is evidence for a particular acquisition mechanism, with discovery and library-construction costs still relevant to a complete comparison.

ProofEvolve (section 5.6) separates two useful reuse experiments. Synthetic compositional families compare a growing library against resetting it. A separate held-out theorem study supplies relevant self-generated, verified proofs as examples and compares them with no examples and random retrieval. That second experiment disables proof-graph search, decomposition and repair, so its measured gain isolates contextual reuse rather than the entire evolving prover. This suggests testing the contribution of an acquired library independently of changes to the surrounding search algorithm.

The multi-agent concept-discovery study provides a complementary mechanism. A conjecturing process guides symbolic regression, a skeptical process challenges regularities by reweighting examples, and provability feedback helps select candidates. Experiments reconstruct expressions related to Euler characteristic and Betti numbers. The provided incidence matrices, dimensions, ranks and nullities already encode mathematical insight. Discovering an expression from those features and inventing the underlying representation are distinct acquisition tasks. A concrete experiment must state which one it measures.

SOAR makes useful teaching an executable development process: a teacher proposes intermediate exercises and is rewarded by measured student progress on difficult training questions. Its initial filtering by repeated failed attempts is an operational criterion, not an impossibility claim. Teacher development and recipient training are separately charged, including unsuccessful curricula. A contributor can therefore be a learned mathematical teacher rather than an unexplained source of ideal hints.

The autonomous comparator must also admit learning during search. TTT-Discover (section 3) updates a model while seeking an excellent solution to the current problem; later generalization is outside that stated objective. ThetaEvolve (section 4.3.1) includes an experiment freezing a checkpoint trained on one mathematical search task and applying it to unseen tasks. These mechanisms distinguish current search progress from retained parameter acquisition. Checkpoint selection and learning costs accompany the latter comparison.

The proposed FTIP experiment combines concept testing, verified lemma accumulation and recipient transfer. This combination is a research proposal, not a result reported jointly by the cited papers. Both campaigns retain the fixed mathematical rules and checker of § [ftip-00ML]; an external contribution may provide a representation, connection or curriculum developed from permitted related experience. Its producer does not receive the withheld evaluation answers. The recipient may reject it, improve it or find an alternative. All of that work belongs to the process being compared.

The finite comparison can show that one developed artifact is useful or affordable relative to tested alternatives. It cannot establish the all-lineage lower bound in § [ftip-00MN]. If an admitted classical solver, a self-generated library or a learned autonomous procedure reaches the same capability more cheaply, that finding is evidence against the proposed advantage for this setting. The correctness criterion does not privilege reconstruction of the evaluator's preferred concept.

A first concrete family can use linear chain complexes over the two-element field \(\mathbb F_2\). This adapts the incidence-matrix concept-discovery setting of Aggarwal et al. into an exact finite experiment. The chosen field, transformations and certificate tasks below are part of this proposal, not a reproduction of that paper.

An object consists of vector spaces of dimensions \(n_0,n_1,n_2\) and matrices \(D_1:\mathbb F_2^{n_1}\to \mathbb F_2^{n_0}\) and \(D_2:\mathbb F_2^{n_2}\to \mathbb F_2^{n_1}\) satisfying \(D_1D_2=0\). All entries, dimensions and allowed operations are public. Arithmetic is exact. Zero-dimensional spaces and zero maps are included. The experiment can provide only matrices and arithmetic, or additionally ranks and nullities; these are different initial endowments and receive separate results. Neither regime establishes discovery of the entire mathematical representation from unstructured observations.

The middle cycles and boundaries are \(Z_1=\ker D_1\) and \(B_1=\operatorname {im}D_2\). The chain identity gives \(B_1\subseteq Z_1\), so the quotient \(H_1=Z_1/B_1\) is defined. Rank-nullity yields

Indeed, \(\dim Z_1=n_1-\operatorname {rank}D_1\) and \(\dim B_1=\operatorname {rank}D_2\); taking the quotient subtracts these dimensions. At the ends, \(\beta _0=n_0-\operatorname {rank}D_1\) and \(\beta _2=n_2-\operatorname {rank}D_2\). These elementary identities explain the evaluator's target and remain withheld as explicit answers where rediscovery is being measured. They are not new mathematical results.

Allowed changes include invertible changes of basis \(P_i\) in each space. They replace the matrices by

The product remains zero and the ranks remain unchanged. Another allowed change adjoins or removes a direct summand consisting of an identity map between two adjacent one-dimensional spaces, with zero maps elsewhere. That summand has zero homology in every degree. Direct sums add dimensions of homology, so these moves preserve all three \(\beta _i\). A candidate invariant can be challenged with new valid objects, basis changes and such elementary additions.

A target asks whether two presented objects are related by a sequence of these allowed moves. A positive certificate lists legal moves and their exact matrices, including inverses for basis changes and the displayed summand for a removal. A negative certificate supplies unequal homology dimensions with checked rank witnesses. A rank witness can give invertible row and column transformations, their inverses and a diagonal normal form with an identity block and zeros elsewhere; the checker verifies these matrix identities and counts the block size. Agreement of a proposed invariant on a few examples is insufficient, and equality of the dimensions alone is not accepted as a positive certificate. The agent must construct the required transformation or another certificate justified by the fixed mathematical checker.

A concrete sampler first draws uniformly from the finite set of nonnegative integer tuples \((h_0,h_1,h_2,r_1,r_2)\) satisfying the declared dimension cap, where

It builds a direct sum of zero-differential spaces of dimensions \(h_i\) in degree \(i\), \(r_1\) identity pairs in degrees one and zero, and \(r_2\) identity pairs in degrees two and one. Independently sampled invertible binary basis matrices scramble this presentation; uniform sampling by rejection from all binary square matrices is one exact choice. The resulting \(\beta _i=h_i\) are evaluator facts, not additional observations supplied to either agent. The distribution and sampling algorithm themselves are public, so reconstructing this decomposition is an admitted strategy.

Positive instances apply a sampled legal move sequence to an object, retaining that sequence privately. At each step the sampler chooses uniformly among the declared finite encodings of dimension-bounded legal moves; the identity move permits padding to the specified length. Negative instances draw two canonical tuples with different homology vectors and randomize their presentations independently. Their dimensions are matched where the chosen profile permits, and results are also stratified by dimension differences to detect easy size cues. Retained rank witnesses certify the labels. The mixture, move count, dimension profile and certificate limits are fixed before final seeds are sampled.

A single middle invariant is not complete even for this family. Objects concentrated in degree zero can have identical \(\beta _1=0\) and different \(\beta _0\), and hence cannot be related by the allowed moves. This provides a concrete counterexample to premature abstraction. A learner may retain the whole homology vector, refine its proposal or use direct algebraic reasoning; successful certification, rather than one preferred formula, determines the outcome.

This initial family has an efficient classical alternative. Gaussian elimination computes bases for cycles and boundaries and decomposes a finite complex over a field into homology summands and adjacent identity summands. It therefore supplies both the invariants and constructive transformations when appropriate. Its arithmetic and certificate costs must be measured as an admitted baseline. The setting can reveal how an agent develops and transfers a method, but cannot support a claim that all autonomous methods face a prohibitive search barrier merely because one language model initially fails it.

The finite family in § 2 permits a complete account of what a contributor learns and what a recipient acquires. Development takes place on earlier instances with independently sampled seeds. The final instance distribution, allowed observations and resource caps are specified before development; target instances and their certificates remain unrevealed. Broad mathematical preparation is disclosed separately from work performed during this experiment.

An autonomous research process alternates candidate generation, experiments and proof attempts. It can propose expressions involving the available matrix features, search for transformations, generate helper lemmas or invent code. A skeptical process selects valid chains that challenge a proposal. Exact counterexamples return a failed instance; a finite test pass only advances a conjecture to a proof attempt. A general lemma enters the verified library only after justification in the fixed proof system. Special-case facts carry their assumptions and are not silently promoted to universal laws.

The library-development loop follows the mechanism of DreamProver: use failed goals to identify helper results, group related discoveries, propose generalizations, verify them and discard redundant material. Suitable discoveries here include behavior under direct sums, invariance under changes of basis, and the need to account for all relevant degrees. Generalization may fail; its attempts, counterexamples and proof costs are part of development. No rule confines the process to discovering the evaluator's homology formula if another certified method is useful.

One executable contributor begins with related finite linear-algebra episodes: solving systems, studying kernels and images, and comparing quotients of nested subspaces. A bounded learner selects useful exercises and retains procedures and justified claims. It subsequently encounters the chain-complex development family and can propose a connection, a proof-producing solver, or exercises that teach the connection to the recipient. Its prior lessons, their solutions and its development work are recorded. It does not receive final target answers, an ideal hint for each instance, or an uncharged completed representation.

A second contribution type is a learned teaching curriculum. Following the progress-based idea in SOAR, a teacher chooses intermediate tasks and is evaluated by improvement of a provisional student on a separate development set. Teacher selection never uses final evaluation outcomes. Useful exercises need not solve the ultimate task directly. Producing and testing them, training provisional students and selecting a curriculum all consume resources. The recipient may receive incorrect suggestions, provided their verification and rejection are included rather than scored as free work.

Separate recipient conditions identify what was acquired. A library condition retains checked statements, proofs and an executable retriever. A procedural condition retains a certified transformation algorithm. A parameter condition updates a declared trainable model using the permitted development material. A combined condition retains an explicitly listed combination. These are different systems, not interchangeable evidence that the same capability has entered model weights. Imported proof macros must expand or be justified under the unchanged checker.

After acquisition, freeze the retained artifact, remove access to the contributor and reveal fresh instances. Measure accepted certificates under a common deployment budget. Test new random presentations within the development size range first, then a separately specified larger-size or composition regime. Success on one does not imply success on the other. A further assessment asks for general laws about direct sums and allowed transformations, with formal proof or independently assessed mathematical arguments as declared in advance. Benchmark prompts and theorem families are held out by mathematical content, not merely renamed variables.

The contributor may itself be an agent, a human or another bounded learning process. What matters is its endowment, development, transmitted artifact and the recipient's resulting capability. Supplying a previously published human proof is a legitimate retrieval condition, but its effect does not by itself demonstrate that a newly developed contributor discovered or taught the method. This distinction permits successful autonomous research to revise the proposed complementarity claim.

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

A campaign's resource record includes model inference, training, mathematical experiments, classical computation, retrieval, contribution production, communication, certificate generation and verification. It also includes failed attempts, discarded checkpoints and validation used to select a method. Model calls alone do not equalize systems using different models, context lengths or training procedures. Record accelerator time, CPU work, human time, money, memory and wall time separately before applying any declared scalar conversion.

Let \(D_A\) denote development work for an autonomous process and \(D_C\) the contributor's charged development. Let \(T\) include transmission, recipient adaptation and validation. For a common deployment budget, write \(E_A(N)\) and \(E_C(N)\) for work on \(N\) fresh instances, including certification. A specified accounting convention then compares

The expression includes any autonomous reconstruction of contributor preparation in \(D_A\). Report inherited preparation and resources treated as sunk separately for both sides. A marginal-session saving does not establish a lifetime saving. If resources remain a vector, compare each component or state a Pareto relation; do not add human hours to accelerator operations without a conversion rule.

At equal task distributions and accepted-success requirements, reuse can amortize a contribution. Under the additional approximation of constant per-instance costs \(e_A\) and \(e_C\), with \(e_A>e_C\), the contributed method has lower total work precisely when

This is an accounting consequence, not a prediction that the inequality holds. If the contributed method has lower success, comparisons must account for the additional work required to reach the same criterion. If its per-instance work is no better, amortization alone cannot erase a larger initial cost. Report failures at a cap as censored attempts; do not turn them into an infinite measured cost or a solved-instance ratio.

The primary acquisition measurement is the fraction of new instances with accepted certificates under the fixed deployment cap. Record it separately for the original distribution and extrapolation regime, along with certificate lengths, work and failures. Repeat complete development campaigns, rather than only decoding from one favorable learned library. Use common evaluation instances for paired comparisons and report variation across development seeds. Cost-to-threshold conclusions require uncertainty for both success and work and must name the procedures and budgets tested.

Additional measurements explain a result without replacing it: which verified lemmas are used in accepted proofs; whether a transformation method handles new presentations; whether the recipient still succeeds without contributor access; and whether a new recipient benefits from the same artifact. A proof differing textually from examples is not by itself evidence of conceptual novelty. Conversely, reuse of a short verified lemma can be a useful acquisition even when that lemma is familiar to mathematicians.

The literature motivates several testable predictions.

1. Relevant verified lemmas should improve recipient performance more than similarly sized irrelevant examples, as suggested by the reuse studies in DreamProver and ProofEvolve. A missing difference would weaken the claimed library mechanism for this family.
2. Challenging conjectures with counterexamples should expose the failure of incomplete invariants, including the middle-degree example in § 2. If a simple algebraic solver already gives equivalent performance at lower cost, this mechanism supplies no cost advantage.
3. A useful curriculum should improve frozen-recipient performance beyond direct exposure to its material at the same accounted resources. If it merely helps while the teacher remains present, the result concerns assisted deployment rather than retained capability.
4. Amortized savings, when present, should depend on reuse count and the deployment regime. Failure on larger compositions would restrict transfer even if the original-size evaluation improves.

A positive pilot would establish a bounded acquisition result for the specified procedures. An autonomous reconstruction at comparable cost would weaken a proposed developmental advantage; a cheap classical solver would defeat an all-method barrier for this family. Neither result decides whether a different mathematical research family admits the separation in § [ftip-00MN]. Moving to that stronger claim requires a new family and an argument covering all equally useful methods, including implicit representations and future model generations.