Developing a method and teaching a recipient [ftip-00NT]

✍️sourceAGENTDRAFTED

The finite family in § [ftip-00NS] 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.