Initial difficulty, discovery and retained capability [ftip-00NR]

✍️sourceAGENTDRAFTED

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.