Consider finite expressions built from a public grammar. A family parameter \(\theta \) specifies local rewrite rules and a distribution of problem sizes and compositions. The description of \(\theta \), the grammar and the rules are available to both campaigns. A target instance asks whether one expression can be transformed into another. An accepted answer contains either a legal rewrite sequence or a proof of impossibility in a fixed sound proof system. The generator produces instances with certificates of bounded size, retains those certificates for evaluation, and reveals only the instance to the learner. The checker, allowed proof rules and certificate-size cap are identical for assisted and closed campaigns.

Public rules make the intended difficulty computational. Earlier experience may teach consequences of the rules that are expensive to find from their description. It supplies no secret governing future answers. The family parameter, development law, evaluation distribution and resource caps are fixed before final seeds are sampled. Developmental and final seeds are independent conditional on \(\theta \). Intermediate learning tasks may be simpler than final tasks, but their relation to the final distribution must be specified by the generator rather than chosen after observing a favorable test result.

One possible learned representation consists of a map \(\phi \) from concrete expressions to abstract states, abstract operations, and procedures connecting abstract reasoning to checked concrete certificates. For example, a learner may discover that several rewrites preserve a quantity, or that large expressions decompose into components with a small interface. A soundness proof for the invariant or decomposition is part of the acquired method when it is used to certify an answer. Recognizing a pattern in a few examples is insufficient. Grounding here means computing the abstract description from the supplied expression and justifying the concrete consequences used by the solver.

The map may discard distinctions. If two expressions have the same abstract description but require different choices, a successful learner can refine the representation, retain a concrete side condition, or use another level of description. The cost of discovering the counterexample and implementing the revision counts. The task family should admit several sufficient methods: another invariant, a different decomposition, a compiled solver or direct search may succeed without reconstructing \(\phi \). Success is measured by checked answers, so equally useful implicit representations in model parameters also qualify.

This is a parameterized family design, not a claimed hard rewrite system. An explicit instance of the construction must give the grammar, rules, certified generator and learning procedures, then prove their performance. Families reducible to a cheap canonical form or direct search may demonstrate learning and transfer while offering no discovery-cost separation. That possibility is a substantive test of the proposed mechanism.

The contributor begins with the disclosed state and bounded development of § [ftip-00NA]. On related rewrite tasks it can propose predicates, execute public rules, test conjectures, build examples and revise its representation. Neither a completed invariant nor a successful curriculum is placed in its initial state unless that preparation is explicitly counted as an inherited endowment. A constructive success argument must describe how the development process produces useful structure with a stated probability, including failed attempts.

Teaching is a further learned action. Let \(Z_t\) be the contributor's retained state, \(h_t\) the observed interaction history and \(q_t\) an intermediate task or demonstration. A teaching policy chooses \(q_t\) from \(Z_t\) and \(h_t\); the recipient's response and checked learning progress supply feedback for later choices. The policy may first teach a distinction on small expressions, then ask for a general invariant, and finally require composition on larger expressions. These stages describe a possible mechanism. Their usefulness must be established for the specified learner, rather than assumed from the apparent pedagogical order.

During development, the contributor can practice with bounded copies of a declared recipient population. It learns which examples correct particular failures and when a new abstraction is worth introducing. The student updates used to evaluate a teaching proposal are real work: cloning, training, progress evaluation, rejected curricula and teacher updates all count. A progress set drawn from the development distribution can provide a verified reward. Final evaluation instances remain unavailable for curriculum selection. Any guarantee must connect development progress to fresh-task success, since a curriculum may overfit either the practiced recipient or its progress measure.

At assistance time, a fresh recipient starts from the declared model endowment. The contributor supplies an explanation, programs, examples or an adaptive sequence of tasks, within communication and interaction caps. The recipient must interpret the contribution, check the relevant claims and learn to use the representation. Evaluation occurs after the contributor is removed. A retained contributed program is allowed when it fits the common deployment interface and cap; merely consulting an uncharged external solver during evaluation is a different experiment.

Useful teaching need not require the teacher to solve the final tasks itself. Conversely, a source that can solve them may still fail to teach the recipient. Measuring the contributor's discovery, its teaching skill and the recipient's later capability separately makes these possibilities visible. A short explanation or a short successful curriculum measures transmission after discovery; its length does not establish that finding it was cheap or expensive.

Current agents already implement substantial parts of this construction. TheoryCoder-2 synthesizes PDDL abstractions alongside a learned Python dynamics model and hierarchical planning. Its discussion nevertheless identifies supplied object-oriented states and brittle predicate grounding as limitations. In its tested environments, an initial observation sufficed for adequate abstractions; learning to revise a representation through unfamiliar interventions remains a further problem. This motivates learning the concrete-to-abstract map, without implying that generated predicates are beyond model capabilities.

ProPlay learns a procedural graph with transition reliability to guide later action. Its failure analysis shows why reusable structure alone is insufficient: a coarse procedure can lose necessary quantitative detail, and a generally reliable transition can be unhelpful for the present task. Its plan is produced once per episode. The representation learner above must therefore be compared with agents allowed to revise plans and abstraction levels, not just with the particular implementation evaluated in that paper.

SOAR, especially its method, ablations and limitations, provides an automated teaching mechanism: teacher tasks receive reward through a student's improvement on a separate hard training set, without the teacher seeing those hard questions. Its substantial bilevel training cost and dependence on a ground-truth progress signal belong in the comparison. Failure on an initial finite sample does not prove that direct discovery is impossible.

Vocabulary Dropout for Curriculum Diversity shows that modifying proposal generation can sustain curriculum diversity, while its asymmetric proposer/solver experiment and verification analysis show that diversity and stronger teachers need not yield better learning. ANCORA combines supervised initialization, proposer/solver training and a filtered curriculum graph for verifier-based learning. Its limitations include diversity collapse within valid outputs and longer-run plateaus. Its Proposition 4.1 assumes continued positive probability of admitting new specifications; that premise does not establish the cost of discovering useful new concepts.

These results motivate a combined comparison with representation synthesis, curriculum generation, active experiments, persistent memory, search and model updates. Their reported benchmarks do not instantiate the rewrite construction or establish its separation. A contributor defined only as a supplier of abstractions, diverse exercises or a curriculum graph would duplicate mechanisms already available to the closed campaign. The remaining question concerns how much work any adequate combination needs to acquire useful structure from the specified starting state.

Fix a final success threshold and a resource vector before comparing methods. The assisted upper-bound problem is constructive: specify bounded development, a prospective source-selection procedure, contribution production and recipient learning, and establish their joint probability of reaching the threshold. Charge failed development and teaching runs where selection uses them. The marginal comparison discloses earlier contributor development separately; a lifetime claim includes that work under § [ftip-00ND]. Communication length, token count, accelerator work and elapsed time are distinct quantities unless an explicit conversion relates them.

Several controlled comparisons can locate the benefit. Giving the recipient a completed grounded representation measures acquisition after discovery. Replaying a successful curriculum measures learning after its selection. Replacing adaptive teaching with fixed examples tests the value of recipient feedback; varying the final expression size and composition tests reuse. A closed campaign that builds its own curricula, revises representations and updates its models tests affordable reconstruction. The supplied-representation and replay experiments are positive controls, not estimates of unaided discovery cost.

The mechanism predicts that a useful developmental curriculum reduces recipient work on unseen compositions, and that failures caused by lost abstract distinctions decrease after grounded refinement. If gains vanish when the source is removed, depend on near-duplicate evaluation instances, or disappear under a cheap alternative solver, the proposed explanation must change. Measuring these outcomes can reject a candidate construction. An observed advantage over the implemented comparison agents still leaves the all-campaign claim open.

For that claim, start with an arbitrary successful closed campaign in Definition [ftip-00MJ]. Its code search, implicit representations, retrieval, synthetic tasks, self-play, active interventions, training updates, heterogeneous models and resource-allocation choices are all admissible when allowed by the declared endowment and caps. The lower-bound argument must connect its checked fresh-task success to work that every such route incurs. It cannot require the campaign to discover the contributor's particular invariant or follow its curriculum. Direct solving is an alternative to conceptual reconstruction.

A family-specific reduction could show that any successful closed campaign solves an independently hard computational problem, while the bounded developmental process and assistance yield an affordable upper bound under the disclosed prior endowments. A restricted representation language or response interface may admit a first, narrower theorem. Neither case permits assuming that every useful curriculum or representation is negligibly likely under arbitrary adaptive search: that would assume the desired discovery barrier. The absence of the contributor's experience in § [ftip-00N8] supplies the starting condition; the prohibitive cost of every equivalent capability is still to be derived.