Fix a specification

Here \(I_0\) contains the initial models, corpora, libraries, prompts, optimizers, evaluators, software and cached results. The nonempty class \(\mathcal C_0\) specifies controller programs and constants available from \(I_0\); it does not grant an arbitrary program chosen after a discovery. An initial generator of additional controllers is allowed, with its generation and selection work charged as explained in § 5.1. The semantics \(\Gamma \) specifies executable operations and costs; \(\mathcal E_0\) specifies baseline observations and tool-response laws. The checker \(V\), task law and reveal schedule \(\mathcal D\), allowed final artifacts \(\mathcal F\), campaign cap \(\mathbf B\) and deployment cap \(\mathbf b_{\mathrm {eval}}\) are fixed before evaluation. Include the no-update procedure as a baseline.

A campaign is a causal execution starting from this endowment. Its state contains available checkpoints, contexts, generated code, retained traces, libraries, optimizer state and resource usage. A controller may use only its charged accessible state: discarded history must be reconstructed at cost. Environment state may remain hidden. All random seeds follow their declared laws; a fortunate completed trajectory is not an available program.

Whenever admitted by \(\Gamma \), operations include model inference, proof and program search, tool calls, parallel workers, memory management, candidate comparison, reward and credit assignment, synthetic tasks, parameter training, architecture changes, and controller replacement. Generated controllers execute under the same semantics and caps. Selection, evaluation and the controller's own computation are charged. These operations may recur in any order; learning need not first produce a complete successful trace or an explicitly verbalized idea.

The lineage is closed relative to \((I_0,\mathcal E_0)\) when its only campaign inputs are scheduled tasks, its randomness and admitted environment responses. This allows computation to reveal useful structure. A simulator using independent randomness is different from a tool observing new hidden world state; the latter access belongs in \(\mathcal E_0\).

Controller selection is independent of unrevealed instance seeds, conditional on declared public family information. This alone does not exclude family-wide answer tables: all such constants and preprocessing belong in \(I_0\). An asymptotic claim specifies uniform generation across instance sizes or explicitly accounts for nonuniform advice and preparation.

For a realized campaign \(\zeta \), let \(\mathbf R(\zeta )\) record inference work, training work, tool and checker work, total accelerator time, peak live memory and storage, peak allocated hardware, wall time and money under the declared operational model. Admission requires

Stop before an unaffordable operation; a missing result scores zero. Charge every failed path, discarded trace, evaluator call, consultation, checkpoint comparison and update. Bound the number of transitions by charged elementary work or an explicit finite horizon: infinitely many free operations are not admitted.

For additive work coordinates, a portfolio costs shared development plus the sum of task-specific work. Shared training is charged once even when it benefits many tasks. Peak resources and elapsed time come from the actual joint schedule, including communication and sequential dependencies. Parallel work is summed across workers. An expected-cost bound does not replace this hard cap.

A scalar budget \(B\) is used only after choosing one resource or a declared conversion with the remaining constraints fixed. Human time, accelerator work and elapsed time have no implicit exchange rate. Model pretraining and contributor expertise may be disclosed sunk endowments in a marginal comparison. A lifetime-cost claim must also account for producing both; unknown historical costs remain unknown.

Fix the statement translation, allowed axioms, formal library and certificate checker \(V\). An answer is a sign \(\sigma \in \{+,-\}\) and a certificate \(p\). Put \(s_V(x,(\sigma ,p))=1\) when \(V\) accepts \(p\) as a proof of \(x\) for sign \(+\), or of \(\neg x\) for sign \(-\); otherwise put \(s_V=0\). The failure output \(\bot \) scores zero. A proof of excluded middle without either signed certificate does not solve the task. A task family may assume one signed certificate exists; independence from the allowed axioms is otherwise a separate source of failure.

For a current portfolio \(x_1,\ldots ,x_n\) with fixed nonnegative weights \(w_i\) summing to one, a campaign \(P\) has discovery score

For one fixed conjecture use a singleton portfolio; its truth need not be randomized. The expectation includes the declared task and execution randomness, with no assumption of independent attempts.

After development, freeze an artifact \(A\in \mathcal F\cup \{\bot \}\) before revealing fresh problems \(x'_1,\ldots ,x'_m\), where \(m\geq 1\). Their identities and solutions are unavailable during development; they are conditionally independent of development draws given the declared task-family variable. With a fixed deployment procedure \(\mathrm {Deploy}\), define

Remove contributor access and feedback into training or checkpoint selection. Any permitted adaptation within one test problem is charged and discarded before the next. Evaluation work counts in the campaign; the per-problem cap is common to both arms. Deployment of \(\bot \) fails.

For model acquisition, \(\mathcal F\) contains learned parameters or adapters with a common fixed harness. For system acquisition it may instead include a bounded acquired library or controller. State which is measured. The pair \((Q_{\mathrm {disc}},Q_{\mathrm {acq}})\) does not allow success on one coordinate to conceal failure on the other. Imported mathematical results and new proof notation require sound translation under \(V\), including the cost of expanding and checking certificates.

Fix the recipient specification, task family, reveal schedule, interaction permissions and resource accounting. Abstract a contributor \(v\) by a causal interaction law, written as budget-indexed kernels

Here \(H\) is the history available to the contributor, \(b\) is its remaining contribution budget, and \(h\) includes the next message or failure/stop output with its joint resource record. The kernels arise from one consistent causal process under stopping: different budgets cannot be assigned unrelated ideal answers. No access to unrevealed test instances or their answers is permitted.

Two internal realizations are equivalent for this abstraction when they induce the same joint laws of transcripts, costs and stopping for every admitted recipient protocol and budget. Mathematically equivalent message contents need not be equivalent interactions: the recipient may find one encoding much easier to interpret or verify. A useful contribution may develop through several exchanges. Producing, interpreting, rejecting, correcting and learning from suggestions all consume resources.

Conditional theorems may assume properties of this interface without simulating a brain or reconstructing a civilization. An unconditional existence result additionally requires a realizable member of the assumed class, for example an executable source with disclosed initial state and costs. A controlled human protocol instead supplies empirical estimates. An arbitrary answer kernel or assumed success probability proves neither.

The target statements, truth contract, checker and reveal schedule stay fixed. Contributors may have different broad backgrounds or search biases; these endowment differences are disclosed. Relevant prior results must be justified under the target checker. A hidden target parameter or precomputed answer table is a different mechanism from conceptual insight. Equalizing all background material is an optional stronger comparison. Giving the recipient textual access to the relevant material can test whether acquiring and using the connection remains costly. Historical preparation follows the symmetric accounting convention in Definition 1.2.

Fix a development law and recipient interaction protocol \(\Pi \) before final evaluation. For development input \(D\) and resulting contribution transcript \(H_v\), choose an independently specified structural predicate \(S(D,H_v)\). Define

A possible property is a sound reduction to a declared tractable class with bounded translation and certificate-expansion costs. A reusable invariant with a proved consequence or a curriculum satisfying a separate learning condition are other possibilities. A fallible analogy may require charged recipient completion before the property holds. The predicate is not simply that the final score improved; soundness, scope and checking costs require their own arguments. Quality is relative to this task, protocol and budget, not a universal ranking of minds.

For \(0<q_0\leq 1\), the restricted class

is legitimate. An existence theorem about a member of this class need not help every contributor outside it. Nonemptiness remains a separate obligation; choosing sources on final test outcomes does not establish pre-evaluation availability. Recruitment and screening costs are necessary when claiming an affordable procedure to find a good contributor, but mere existence does not require a population recruitment theorem.

To discuss a median, additionally declare a population law \(\mu \) on admissible contributors with measurable quality \(v\mapsto q_v\). Let \(q_{50}\) satisfy \(\mu (q_v\leq q_{50})\geq \frac 12\) and \(\mu (q_v\geq q_{50})\geq \frac 12\). Then define

If \(q_0\leq q_{50}\), this class has at least half the population mass. If \(q_0>q_{50}\), even nonemptiness needs evidence. The median can be zero, so belonging to the upper half alone does not guarantee useful assistance. There is no default uniform law over all possible contributors, and an unattained quality supremum need not have a best contributor.

Fix one contributor and one recipient protocol with almost-sure total resource caps, including failed consultations. Let \(Z\in [0,1]\) be the realized fresh-task score of its frozen artifact with contributor access removed. Suppose, for the same joint process and remaining resources,

Then \(Q_{\mathrm {acq}}=\mathbb E Z\geq q_0\beta \).

No independence assumption is used. A uniform recipient guarantee for qualified transcripts and compatible development histories can establish the transfer premise, including interpretation, verification and acquisition costs. A guarantee for a different, easier message distribution cannot.

Together with a universal closed bound \(Q_{\mathrm {acq}}(P)\leq \tau ^-\) and an admissible member of \(\mathcal G(q_0)\), the strict inequality \(q_0\beta \geq \tau ^+>\tau ^-\) yields the assisted crossing in § 4. The substantive obligations are affordable source quality, recipient transfer and the bound over every admitted unaided alternative. The elementary expectation inequality alone establishes none of these.

Fix a scalar accounting model with the other constraints declared. Suppose an admitted assisted campaign \((R,v)\) at total budget \(B\) has an admitted closed simulator at budget \(g(B)\). Require that the simulator can reproduce the contributor's endowment, observations and causal interaction, together with the recipient's allowed final artifact and evaluation law. All simulation work and initialization count. Then, for \(j\in \{\mathrm {disc},\mathrm {acq}\}\),

If the simulation is uniform across instance sizes with \(g(B)\leq cB\) for a fixed constant \(c\), an actual assisted procedure reaching \(\tau \) at work \(U(n)\) implies \(B_{\mathrm {closed}}(n,\tau )\leq cU(n)\). This excludes a lower bound \(L(n)\) with \(U(n)/L(n)\to 0\). Unavailable background state, observations, hardware or large simulation overhead can invalidate the premise; different origin alone does not. The argument does not assume that a language model already has an affordable simulation of a human contributor.

Admission includes discovery of any required reconstruction program from the declared initial state. A simulator written with advance knowledge of the useful representation does not satisfy this premise merely because its later execution is cheap. If the program is generated during the campaign, its generation law, failed attempts and selection costs belong in the simulation. This conditional proposition supplies no lower bound on that discovery cost; § 5.1 distinguishes program existence from its availability to the lineage.

In this exchange, the human is the contributor and the agent is the recipient: the system receiving and processing the contribution. The agent's proposals arose within an already human-directed conversation; they were not outputs of a separate unaided experiment.

1. The agent proposed a resource-bounded formulation and a finite missing-evidence construction. The human rejected missing facts as the intended mechanism and described conceptual leaps across model generations: new perspectives, paradigms and connections between domains. The agent revised the target to conceptual discovery and separated prohibitive finite work from permanent unreachability using the enumeration countercheck.
2. The agent specified an executable source with bounded observations. The human challenged an oracle-like abstraction, pointed to diverse cultural backgrounds and developed representations, and asked for an abstract account of what the source contributes. The agent formulated the causal contribution interface, with background differences disclosed rather than a mandatory model of a brain or lifetime.
3. The human emphasized that existence of good contributors need not imply usefulness of all contributors, and suggested an upper-median restriction. The agent separated independent structural quality, class nonemptiness and recipient transfer, while showing why a median requires a population and need not have positive quality.
4. The human suggested studying recursive self-improvement papers for the gap between the problems they diagnose and the portions their methods repair. The agent examined contemporary work and checked a revised primary source that narrowed stronger self-imitation claims. The resulting thesis distinguishes affordable quality, recipient acquisition and a universal unaided bound, with proof, refutation and precise obstacles all possible.

In Definition 3.1, \(H\) corresponds to the exchange so far and \(h\) to the human's next criticism, analogy or research direction. The agent's retained conversation and revised artifacts form its evolving state; reasoning, literature search and checking are its processing actions. The human did not supply a completed theorem: the assistance changed the problem representation and choice of inquiry. The observed outcome was a revised conjecture, before any fixed-target acquisition experiment. No structural-quality probability, cost advantage, held-out acquisition score or universal unaided bound was measured, so it does not establish the separation conjecture.

The initial controller class in Definition 1.1 is part of the endowment. It is not enlarged after an assisted discovery by inserting a program tailored to that discovery. A concrete specification can supply a finite collection of initial controllers, or an executable procedure that generates further controllers. In the latter case, generation, execution, comparison and selection occur within the campaign and consume its budget. The generator's fixed code and constants are themselves initial resources.

For example, let a campaign generate a program \(A_Z\) using a random variable \(Z\), and let its later interaction depend on the observed results. Its score averages over that declared generation and subsequent execution. Showing that one realization \(A_z\) constructs a useful representation cheaply does not show that the campaign finds that realization cheaply. Replacing the campaign by this selected program changes the initial endowment unless a legal route to its availability has been supplied.

This distinction does not forbid an ingenious algorithm. A procedure already admitted from the public task-family description is a legitimate closed alternative even if nobody has tested it. A lower bound must cover it. Conversely, a proof quantifying over all programs with arbitrary family-specific constants grants more advice than a fixed model lineage possesses. Uniformity across input sizes does not alone remove that advice: a single finite program can already contain the decisive family-wide idea. The theorem must state which controller access it grants.

An existential mathematical upper bound may describe a particular admitted program without proving that a person will discover its proof. The operational claim that a fixed lineage can acquire that program is stronger. It requires an available initial program or a charged causal construction from its accessible state. Keeping these claims distinct prevents both free advance knowledge and the exclusion of legitimate internal discoveries.

Fix a difficulty \(n\) and task-family parameter, the truth contract, fresh evaluation law and deployment cap of Definition [ftip-00MM]. For an allowed frozen artifact \(f\), including the failure artifact \(\bot \), let \(q_n(f)\) be its expected fresh-task score under that evaluation. The expectation includes fresh tasks and deployment randomness; set \(q_n(\bot )=0\). Evaluation begins with exactly the retained state permitted by the specification. Define

If the comparison randomizes a shared family parameter, apply this definition conditionally on that parameter and then average the resulting scores. This class is defined for mathematical analysis; membership need not be decidable or cheaply recognizable during research. It includes any artifact with the required performance: explicit lemmas, learned libraries, new architectures, implicit weights, and methods that avoid the contributor's representation entirely, whenever those artifacts are allowed.

For a random final artifact \(F_P\), the acquisition score is \(Q_{\mathrm {acq}}(P)=\mathbb E[q_n(F_P)]\). The desired lower bound must control this expectation for every admitted closed campaign. It cannot merely show that one named representation is unlikely to appear. Nor is a bound on reaching \(\mathcal U_{n,\tau }\) automatically a bound below \(\tau \): many outcomes just below the threshold can still have high mean score. A proposed proof must connect its event or structural quantity to the complete score distribution, as the explicit hypotheses of proposition [ftip-00MP] illustrate.

The contributor need not transmit an entire solution. A question, analogy or example may change which experiments the recipient attempts. The resulting interpretation, validation and learning remain charged. Acquisition is established only by the frozen recipient's performance on fresh instances; an insightful exchange by itself establishes neither that performance nor a lower bound on unaided discovery.

The proof direction is to begin with a concrete developmental asymmetry: some task-relevant experience available to a contributor is absent from the lineage's initial data and observed traces. From a specified family and computational model, derive that acquiring any equally useful capability exceeds the closed budget. The absence of that experience is a premise. The absence of every affordable substitute is the desired conclusion, and must not be included as another premise.

Three arguments are needed. A bounded developmental process must produce reusable structure with a stated probability before fresh target instances are revealed. A charged interaction and learning procedure must turn that structure into recipient capability. A lower-bound argument must cover all closed histories admitted by the initial endowment and execution semantics, including adaptive tools, simulations, generated programs, training, changed architectures and alternative representations. The first two arguments describe a constructive assisted procedure; the third establishes why the closed lineage cannot match it at the chosen resources.

A necessary-event estimate becomes useful only after the family and operations justify both its necessity and its probability bound. Assuming that every successful route requires a rare conceptual event simply moves the central difficulty into an assumption. Likewise, absence from a corpus does not imply computational inaccessibility: affordable experiments or derivations may supply a substitute. A proof must explain what the particular environment makes accessible and why the admitted closed operations cannot obtain an equally useful substitute within budget.

Both inequalities in § 4 remain open for the intended conceptual-discovery mechanism. The conditional transfer estimate in proposition 3.3 and simulation proposition in proposition 3.4 do not prove them. The research objective is a positive separation proof, beginning with a sufficiently concrete account of development, access and cost. Any restriction used to make the mathematics tractable must be visible in the claim; a result for a narrow action class does not establish a ceiling for all model lineages.

Specify a developmental process by an architecture, initial state, learning and action rules, an environment response law, and hard resource caps. The process generates an interaction history and a retained state \(Z\); from that state it induces a contributor \(v_Z\) of Definition 3.1. States include learned parameters, habits, libraries and memories. Their existence must follow from the declared development, rather than from choosing an arbitrary helpful state after seeing the evaluation.

An initial library or teacher may already embody earlier learning. Treat that preparation as a disclosed inherited endowment, or include a bounded process producing it. The controlled comparison must not credit the current environment with structure already present before development begins.

Development may include other learners, teachers, language, tools and related tasks. Their response laws and relevant preparation are part of the specification. The source's developmental randomness, failed learning and failed contributions remain in the joint score distribution. An existence claim can supply one explicit developmental process with a proved quality guarantee. Selecting a lucky realized graduate is different: an affordable selection procedure must account for screening and failures, as in Definition 3.2.

A task-family parameter may be shared between development and fresh evaluation, allowing experience to be relevant. The development law and source-selection rule are fixed before final instance seeds are sampled. Conditional on the declared family parameter, those seeds are independent of development. The contributor receives neither the unrevealed instances nor their answers. Broadly useful structure acquired on earlier tasks is allowed; a secret determining the final answers is a different mechanism from the conceptual discovery sought here.

To isolate the environmental contribution, one controlled comparison starts copies with the same architecture, initial state, learning rules and development caps, then varies only their environmental access. This can establish an environmental effect for those processes. The lower-bound claim is stronger: it must still cover every closed campaign admitted by Definition 1.1, rather than only the one control learner used in that comparison. Architecture, initial artifacts and permitted learning changes must remain explicit when moving from this control to a human–model study.

The starting asymmetry concerns available experience: the lineage's initial corpora, memories and recorded traces do not contain some relevant part of the contributor's development. Literal absence is only a weak condition. Another description, a simulation, a derivation or a different experience may make an equally useful capability affordable. The claim in § 5.3 is to derive a bound covering these substitutes.

Three kinds of access should be distinguished. A stored trace gives particular observations and actions. Interactive access lets a learner choose actions based on its current state and receive the corresponding responses. Access to an executable environment model permits simulations, subject to the cost and fidelity of that model. None is automatically identical to either other kind: a finite trace need not determine responses to untried actions, while an accurate model can sometimes replace direct experience. Declare what the baseline actually has.

If environmental responses reveal a hidden bit that fixes the target answer, an information bound may be possible, but it proves a different mechanism. For conceptual discovery, retain a common mathematical truth contract and ask how development reveals reusable ways to search, represent or reason. The baseline may already contain enough information to compute the answer in principle. The proposed gap concerns the resources required to find and acquire an effective method.

A compact description of the acquired structure need not imply a cheap route to it. Description length, execution cost after identification, and discovery cost are different quantities. Conversely, declaring the structure absent from all affordable computations would assume the desired conclusion. Its inaccessibility must follow from the concrete task family, the supplied endowment and the admitted operations. Tools and simulations are charged operations within that argument, not an additional process outside the comparison.

A realistic comparison needs more than the contrast between a person who grows and a model that reads text. Human experience is selective and changes with the learner's actions and abilities. Models also inherit large bodies of human-produced data and can learn from video, interaction, feedback, generated tasks and earlier model generations. The relevant asymmetry is the particular developmental access and retained structure available in the specified comparison.

Smith and colleagues' 2018 review, The developing infant creates a curriculum for statistical learning, describes head-camera and eye-tracking evidence that infants' visual inputs change with posture, mobility and object manipulation. It proposes that these changing inputs can support a developmental curriculum. The authors leave the causal benefit of particular ordering and its relation to learning mechanisms as research questions. This motivates modelling learner-dependent experience; it does not establish an adult mathematical advantage or a lower bound for artificial learners.

Artificial learning already combines different forms of experience. In V-JEPA 2, Assran and colleagues pretrain visual representations on large-scale video, then train an action-conditioned predictor with robot interaction trajectories. The result supports planning for evaluated manipulation tasks. The relevant lesson is that recorded observations, action information and learned simulation can play different roles within one model's development. These results do not by themselves concern mathematical concept discovery.

The SIMA 2 report of November 2025 describes learning in new game environments using self-generated experience, with Gemini supplying tasks and estimated rewards, after initial learning from demonstrations. This is an example of a model lineage gaining skills through further interaction. Its teacher, environment access and retained experience belong in the baseline when available. The reported remaining difficulties with long tasks and memory are properties of that system, not universal limits of model growth.

These observations suggest comparing concrete interventions: preserve or shuffle a developmental sequence; provide selected traces or interactive access; add a bounded teacher; allow the lineage to design its own curriculum. Fix total resources and evaluate fresh-task acquisition after removing help. Such comparisons can identify which experience matters and guide a mathematical family. Even a large measured gap applies only to the tested procedures; proving the closed inequality still requires the broader argument in § 5.3.

A marginal comparison begins with a specified pretrained lineage and an already-developed contributor. It charges the closed campaign's new search and learning, and the assisted campaign's contribution production, failed help, communication, interpretation, checking and learning. Both face the same final evaluation and resource accounting. Their prior histories are disclosed endowments. A gap here means that assistance makes new acquisition affordable from those starting states; it does not mean that producing the contributor was cheaper than producing the model.

For an additive scalar work measure, let \(D_M\) be the model lineage's prior development, \(D_C\) the contributor's prior development not already included in \(D_M\), and \(W_0(m)\), \(W_1(m)\) the closed and assisted marginal work for a specified portfolio of \(m\) tasks. With any shared preparation charged once, the corresponding lifetime totals are

Thus \(W_1(m)<W_0(m)\) need not imply \(T_1(m)<T_0(m)\). Shared expertise may be amortized across a declared portfolio; one cannot divide its cost by an arbitrary number of hypothetical future beneficiaries. Human-created training data, cultural resources, teachers and infrastructure follow the same inclusion convention on both sides. Unmeasured historical costs remain unmeasured.

The full resource comparison is a vector as in Definition 1.2. Human time and accelerator work need an explicit conversion before a scalar inequality compares them. Wall time, peak hardware and memory follow the actual schedule, including causal dependencies. A model may copy states and run many experiments in parallel; an environment may impose an interaction rate. Whether simulation or accumulated experience can remove that delay is part of the setting, not an assumed advantage for either side.

A first proof target is marginal assistance, with bounded prior development specified separately. A lifetime comparison is a stronger additional question. Even with identical architectures, environmental access and prior duration can differ; equalizing architecture alone does not equalize all costs. State whether a claimed prohibitive expense is work, money, memory or elapsed time, and give the corresponding operational cap.

A promising mathematical setting couples related developmental tasks to a fresh target family through reusable structure. The contributor must acquire that structure by a bounded process. The recipient must then learn to use it under the common checker. The central choice is a family whose structure can both explain the developmental benefit and support a lower bound over the admitted closed alternatives. The following possibilities are research directions, not established separations.

One direction is a family of transformation puzzles with public local move rules. Development offers related tasks on which a learner can experiment, notice conserved quantities or discover a compositional decomposition. Fresh tasks ask for a checked move sequence or a certificate of impossibility. The acquired method must apply to new instances, and its certificates must fit the shared checker and deployment cap. This makes the intended assistance concrete without giving the contributor unrevealed answers. The missing argument is why the closed lineage cannot affordably discover any comparably useful invariant, decomposition or direct search method from the same public rules and its admitted tools.

A second direction studies the order and interaction of developmental experience. A learner's partial understanding can determine which question or intervention makes the next relation visible. Compare that process with the available passive traces and with any interactive or simulated substitutes admitted to the closed lineage. A proof must derive the cost of obtaining enough useful experience or processing the available data; simply withholding the interaction and declaring its outputs necessary would not explain conceptual discovery. Giving the lineage the same interaction channel is a stronger comparison when the intended mechanism is the cost of choosing how to use it.

A third direction studies a contributor drawing on cumulative cultural search. Several bounded learners develop, test and teach reusable concepts across earlier tasks. A current contributor's short suggestion may transmit structure produced by that longer process. This naturally motivates a marginal advantage and an amortization calculation. A lifetime advantage additionally requires accounting for that earlier population's work and for analogous shared data, teachers and parallel search available to model lineages. Culture must be generated by the declared process; a collection of perfect hints would assume its success.

For each direction, the proof needs a quantity that can be bounded through every admitted operation and connected to fresh-task performance. Information arguments apply when there is residual uncertainty; query arguments apply to explicitly limited response interfaces; computational arguments must address the available program class and its costs. If a separation is conditional on an independent computational hardness assumption, state that assumption and exhibit the reduction. Merely renaming the desired discovery difficulty as a hardness assumption adds no explanation. Restricted models can yield useful first results, provided their restrictions are not silently transferred to contemporary agents.

The most immediate constructive target is a development process that learns a reusable invariant on one task distribution and transfers it to fresh certified tasks. Alongside that construction, seek a family-specific lower bound covering every equally useful acquired method as in § 5.2. Keep the model's own discovery, simulations and learning inside this argument. Neither the construction alone nor a failed search for substitutes proves the prohibitive closed cost.

§ 7 develops the first direction as a representation learner whose developmental experience also teaches it to construct a useful curriculum for another recipient. The concrete objects are the grounded representation, the learned teaching policy and their fresh-task effects.

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 § 6.1. 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 § 6.4. 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 1.1. 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 § 5.3 supplies the starting condition; the prohibitive cost of every equivalent capability is still to be derived.

Extend the public rewrite setting of § 7.1 by a sequence of demand states \(X_t\), with a declared initial distribution. A fixed transition law \(K_\theta \) governs how the demand state changes. Conditional on \(X_t\), a fixed generator \(G_\theta \) samples a certified task. The parameter \(\theta \), both laws and the rewrite rules are available to both campaigns. A demand state may favor particular compositions, expression sizes or interfaces, so an abstraction useful in one period need not remain useful in the next. The future random seeds are unrevealed, and the laws are fixed independently of either learner's decisions. The laws are given as computable programs; their execution and any derived approximation are charged.

For example, demand may move between tasks dominated by local cancellation, tasks requiring repeated composition, and tasks coupling several components through a shared boundary. This describes possible structure in the generator, not established difficulty of those tasks. The change law could make a local regularity predictive of later coupling, so acquiring a compositional representation has value before that coupling becomes common. An actual construction must specify the expressions, rules and transition probabilities, and show that its proposed investment really reduces later work.

A state \(X_t\) can be observed directly or inferred from the common history of revealed tasks and responses. Fix which case applies. If the state is latent, both campaigns receive the same observations; the source has no private reading of the current state or future seed. In the computational version, their problem is to process the available history and public laws cheaply enough. Uncertainty remaining even for an unlimited observer is common to both. Giving only the contributor an informative sensor or an undisclosed generator defines a separate information-access comparison.

Development uses earlier independently seeded episodes from the declared process family. It may teach a learner to recognize which histories predict useful future structure, but cannot supply the final episode's hidden state. Selection of the source and its retained state precedes final seeds. During evaluation, tasks arrive in order; any feedback and adaptation available after an answer follow the same specified schedule on both sides. The final correctness predicate, proof rules and certificate cap stay fixed throughout the changing demand distribution.

A developmental learner retains a predictive state \(b_t\) and a library \(L_t\) of representations, subroutines or reusable reasoning procedures. From the observed history it updates its forecast of future tasks and decides whether to extend, refine or discard library elements. The forecast need not be an explicit Bayesian posterior, and the library may be encoded in parameters. The defining feature is that the learner uses anticipated downstream utility in deciding what to acquire.

The two learning problems interact. A new representation can make a previously obscure regularity in the task process easier to recognize; a revised forecast can change which representation is worth learning. Consequently, a predictor operating over a fixed, human-supplied list of perfect abstractions removes part of the proposed acquisition problem. A bounded construction should describe how candidate structure is generated, how its consequences are grounded, and how experience updates both prediction and selection. Initial program libraries, pretrained predictors and demonstration histories remain disclosed endowments.

One possible developmental procedure generates candidate decompositions from earlier solved tasks, predicts their usefulness over a finite future horizon, and spends a capped amount of work testing the most promising candidates on independently sampled continuations. Failed predictions supply feedback. This is an explicit algorithmic pattern, not a free forecast oracle: generating continuations, constructing a simulator, evaluating candidates and revising the predictor all cost work. With public computable laws, the closed campaign may implement this procedure too. The intended advantage must come from the cost of acquiring a sufficiently useful procedure from the specified endowments.

A developed contributor can teach the recipient its selection method, transmit a grounded library with its conditions of use, or help initialize a predictor. The recipient must acquire and apply the contribution within the assistance cap. Later library selection and task solving are performed without further uncharged source access. A one-time selection for a revealed history is a weaker form of help than learning a reusable prospective policy; transfer to fresh episodes distinguishes them. Neither form requires matching the source's internal concepts.

Prospective Compression in Human Abstraction Learning studies reusable-helper choices while a latent curriculum changes. Its two controlled Pattern Builder experiments involve 60 participants in total and six computational comparison models. The results support sensitivity to future reusable structure beyond the tested retrospective and LLM-based accounts. They motivate studying prospective acquisition rather than only compression of earlier solutions.

The paper's limitations are decisive for the comparison here. It does not implement a full learner that infers the latent task-generating process, and individual tasks can be solved without reproducing human helper choices. Its restricted helper-optimization hardness result does not bound arbitrary learning agents. The proposed construction therefore evaluates checked future performance and total work, rather than similarity to human-selected helpers, and admits agents that jointly learn a process model and a library.

Such agents may forecast by Bayesian inference, learned world models, sequence prediction or simulation; select structure by search, expected utility or learned value estimates; and retain experience in memory or model updates. ProPlay supplies one contemporary procedural-memory mechanism, while BREW constructs reusable recipes from trajectories and optimizes their correctness and retrieval usefulness. These particular systems do not establish prospective learning for the public rewrite process, but their mechanisms are available components of an alternative campaign.

Theoretical active-inference guarantees also require attention to what is already supplied. Curiosity is Knowledge proves results under stated identifiability and regularity conditions; its discussion identifies idealizations including a discrete hypothesis setting and exact mutual-information computation. Providing an adequate hypothesis class or an exact acquisition calculation can remove work that the developmental construction is meant to explain. Conversely, these restrictions do not establish that a more general agent cannot find an affordable approximation or a different sufficient method.

Informative experiments can improve either representation discovery or forecasts of future demand. A contributor may learn which intervention distinguishes plausible decompositions or exposes a misleading progress measure. In the public-rule setting, both campaigns can execute the same permitted experiments; the question is the cost of choosing and interpreting them. Criticality-guided learning learns to target failure-prone conditions from execution outcomes, showing why rarity under random sampling is too weak an argument. Its predefined state representations remain a relevant limitation of that implementation. A physical experiment with unequal access may support a different, explicitly informational or interaction-rate result.

Cultural preparation can supply earlier exploration, tested concepts and teaching practices. Model it as a bounded population that generates, selects and transmits methods, or disclose its products as inherited endowments. Failed discoveries, selection and transmission count; so do analogous shared data, model populations and libraries on the closed side. The study of AI-discovered strategies in human culture separates difficulty of discovery, ease of transmission and recognizable advantage. Its AI-to-human direction supports an origin-neutral contribution. Neither that experiment nor its population simulations establish a general discovery lower bound. Prior cultural work can explain a marginal benefit, while lifetime and amortized claims require the accounting in § 6.4.

Research judgment can help choose a fruitful subproblem, recognize when an abstraction loses an essential distinction, or improve an intermediate progress measure. Such choices affect how computation is spent; they do not change the final mathematical task or checker. The study of divergence and negation in scientific ideas reports differences between expert ratings and several automated evaluations, while also showing benefits from learning a reward model on human ratings. This motivates acquired judgment without treating it as a human monopoly. Expert ratings of ideas do not directly certify mathematical discovery. For this construction, any learned progress measure must justify its value through fresh checked outcomes, with its own training and validation charged.

These three contributions have distinct roles: experiments produce useful evidence, culture explains how prior useful structure was generated and transmitted, and judgment guides selection and evaluation. They can support both major constructions, but their benefits do not automatically add. A curriculum learned from cultural demonstrations and selected by an experimental progress measure may share preparation across all three. Ablations should vary one mechanism at a time, and total accounting should charge shared work once.

Fix a horizon \(H\), a success threshold and a common adaptation schedule. In an additive work measure, let \(A_t\) charge forecasting, experiments and library construction before task \(t\), and let \(S_t\) charge solving, checking and permitted learning from that task. Let \(I\) charge assistance production, communication and recipient acquisition. The assisted marginal work is

The closed total charges its corresponding acquisition and task work under the same convention. Forecasts may optimize expected future work, but a hard budget claim must also bound realized resource use and include runs that exhaust the cap in the success probability. Memory, peak hardware and elapsed time retain their separate operational constraints. Earlier development and any portfolio amortization follow § 6.4.

A useful prospective policy should reduce later acquisition and solving work enough to repay its earlier investment at the fixed success threshold. Compare it with retrospective compression, a learned generative-model policy, direct solving without a reusable library, and a campaign that constructs its own predictor and representations. Equalize current observations and disclose earlier preparation. An oracle given the future sequence can diagnose the maximum possible value of anticipation, but its performance does not establish that either real learner can obtain it.

The mechanism predicts a larger benefit when demand changes have learnable structure and the right abstractions require substantial advance investment. It predicts a smaller benefit when demand is uninformative, useful libraries are cheap to build on arrival, or direct solving already fits the cap. A predictor can be accurate yet unhelpful if its forecast does not change an affordable decision. Measure fresh-task success, realized work and the effect of forecast-guided investment together. These are testable predictions for the specified process, not reported experiments.

The constructive proof problem is to produce a bounded developmental learner and establish its later performance without hindsight selection or privileged final-episode information. The closed lower-bound problem must cover every equally useful selection or solving method in § 5.2, including implicit forecasts, alternate abstractions, heterogeneous learners and internally generated curricula. A lower bound only against retrospective compression would explain that restricted comparison, not the conjecture about contemporary closed campaigns.

For a computational separation with public laws, a reduction must connect fresh checked success to an independently hard inference or computation problem under the declared endowment and resource cap. It must also explain why direct solving and alternative investment policies cannot avoid that work. Withholding the future law from one side, choosing future tasks after seeing its library, or assuming every useful forecast is rare would establish a different claim or assume the desired conclusion. The prospective construction supplies a distinct acquisition problem; the all-campaign cost inequality remains open.

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 § 2; 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 § 4. 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 § 9.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 § 9.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 § 9.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 § 4. Moving to that stronger claim requires a new family and an argument covering all equally useful methods, including implicit representations and future model generations.

Fix \(B\in \mathbb N\) charged elementary transitions and a \([0,1]\)-valued realized acquisition score \(Z\), including its evaluation randomness. Let \(G_t\) mean a specified necessary structural event has occurred by transition \(t\). Assume \(G_0\) is false, \(G_t\subseteq G_{t+1}\), and \(Z\leq \mathbf 1_{G_B}\) almost surely. For deterministic \(\epsilon _t\in [0,1]\), suppose that every admitted campaign and every permitted positive-probability history before \(G\) satisfy

For general history spaces use the corresponding conditional-kernel bound almost everywhere for each admitted campaign. Include histories after training and controller replacement. Stopped runs are padded by absorbing transitions. Then every admitted \(P\) satisfies

If the premise holds with \(\epsilon _t=\epsilon (n)>0\) at every work budget, then \(B_{\mathrm {closed}}(n,\tau )\geq \frac {\tau }{\epsilon (n)}\) for integer work budgets. A bound measured for one fixed checkpoint does not supply this premise. If other routes can achieve positive score without \(G\), the domination assumption fails. Calling \(G\) simply “success” does not explain a discovery mechanism without an independent probability bound. Recognition and learning obstructions may require other arguments.

Let \(\mathcal R\) be a measurable set of complete states. Suppose the initial state lies in \(\mathcal R\) almost surely, and every admitted transition from a permitted history ending in \(\mathcal R\) remains in \(\mathcal R\) with probability one. Suppose no successful terminal state lies in \(\mathcal R\). Then for every admitted campaign,

Fix a target with a finite accepted signed certificate under a decidable checker. If the baseline admits enumeration of all finite signed candidate strings over a finite alphabet in increasing length, checking each in finite time, then some admitted procedure discovers a certificate in finite total work.

This assumes enumeration and checking have the required memory and other resources as work grows; it does not override fixed hardware caps. It gives no useful realistic work bound and no fresh-task acquisition guarantee. Short compressed proofs may still be expensive to expand.

Independent restarted attempts of uniformly bounded cost with fixed success probability \(p>0\) have expected attempt count \(1/p\). Full token support alone does not establish restart access, termination or such a fixed probability for an adaptive lineage. Other processes can succeed almost surely with infinite expected time. Neither one slow process nor one failed search bounds all admitted alternatives.

Hemmer and colleagues distinguish available complementarity from benefit actually realized by a human–AI team. They also distinguish differences in information from differences in capability, and choosing an individual's answer from producing an answer neither individual supplied alone. This motivates the separation between Definition 3.2 and proposition 3.3: a source can expose useful structure while the joint procedure fails to exploit it. Their decision-making experiments do not establish learning into successor models.

In Semantic knowledge guides innovation and drives cultural evolution, Yaman, Tian and Lindström combine an agent-based model with a 1,243-participant experiment. Meaningful item depictions let participants use semantic knowledge; abstract symbols obscure it while preserving combination rules. Semantic knowledge and social learning support cumulative innovation. The model gives a concrete mechanism: learned representations direct exploration, and socially transmitted examples improve those representations across generations. The evidence comes from a closed-world recipe task. The authors also warn that strong priors may hide counterintuitive combinations. Cultural background is therefore a possible source of directed search, with relevance and flexibility still to be established.

Unlocking LLM Creativity in Science through Analogical Reasoning makes cross-domain object and relation mappings explicit, then searches for candidate solutions. It reports diversity and judged-novelty gains and four biomedical implementation case studies. Its cross-domain baseline also uses two model calls; its unconstrained baseline uses one. These counts help interpret the comparison without establishing matched total cost. Feasibility and later acquisition remain separate questions. Because the model itself constructs analogies, this method also belongs among the closed lineage's possible substitutes for an external contributor.

A testable hypothesis is that assistance helps when it supplies a relevant relation the recipient can verify more cheaply than it can discover. Compare a supplied relation with internally generated analogies at matched total cost. Give both arms the relevant background texts in a further comparison, charging retrieval and interpretation. If the advantage persists, access to texts alone has not explained it; if it disappears, this instance supports a background-access explanation. Neither outcome by itself bounds all admitted internal search procedures.

A contributor may offer a promising question or a direction of inquiry without knowing its final answer. The difficulty is prospective: the learner must choose where to spend effort before observing how much that effort will teach it. Surprise can prioritize noise, while measured learning progress arrives after the investment.

Herrmann and Schmidhuber model interestingness through complexity–runtime profiles and future compression progress under specified Length, Algorithmic and Speed priors. Their analysis and finite enumeration experiments study when present structure predicts further compressibility. Section 4.4 limits the formal correspondence through Busy Beaver time scales; a long plateau does not exclude a later breakthrough. The analysis supplies neither an affordable selector for frontier models nor a lower bound over their possible research strategies.

For the contribution model, a direction's quality needs an independent property: for example, a reduction exposing a learnable subproblem with bounded translation cost. Calling a direction “interesting” cannot supply that property for free. An informative experiment would compare equal-cost choices by the recipient, a contributor and a shuffled-direction control, then measure verified progress and fresh-task performance after a fixed learning budget. A plausible prediction is that a useful structural selector outperforms mere surprise when high-surprise distractors are present. A successful internal selector weakens the proposed external advantage for that specification.

Recursive Harness Self-Improvement addresses the cost of maintaining effective agent workflows and the need for useful execution traces in model–workflow co-evolution. It revises prompt-level workflows from pairwise evaluation history while holding the foundation model fixed. Experiments on 30 synthetic machine-learning research tasks show gains over the tested configurations. The proposed information-theoretic explanation is a hypothesis. Its conclusion leaves internalizing the resulting traces into future foundation models for future work. The improved workflow is evidence of better system behavior; successor-model acquisition needs a further result.

Mendel Gödel Machine diagnoses a different missed opportunity: editing from a single failed trajectory underuses comparisons across tasks and lineages. Its operators extract evidence from both kinds of comparison to edit agent scaffold code. The diagnostic theory assumes informative comparisons and an editor able to use them. Its simulations vary the comparative fixing advantage, including a null setting with no advantage, and its coding-agent experiments test bounded benchmark subsets. This is a concrete internal remedy, not evidence that every archive automatically yields useful structure.

These methods suggest an acquisition experiment with declared artifact types. First measure the improved workflow with its persistent instructions and memory. Then train a successor on the resulting traces and evaluate that frozen successor under the same declared deployment wrapper, with contributor access removed. An unchanged-weights comparison and a successor trained from baseline traces distinguish workflow effects from learning effects. All trace generation, evaluation, selection and training consume the lineage budget. A gain that survives the second comparison supports acquisition under that contract; a workflow-only gain still counts when workflows are among the allowed final artifacts in Definition [ftip-00MM].

A second prediction concerns archive quality: comparisons should help most when failures share an identifiable cause and the archive contains a relevant contrast. Vary those conditions while matching archive-building and editing costs. Successful internally generated comparisons must enter the closed baseline before attributing an affordable advantage to an external source.

Beyond Final Scores studies seven models on 36 long-horizon AI research and development tasks. Its process diagnostics separate framing, execution and feedback; its experience comparisons include continuations with retained versus erased experience and lessons transferred to held-out tasks. Reuse can help or mislead. Under its particular novelty review, three of 252 best-seed solutions qualify as novel approaches. This finite observation identifies a problem in the tested setting, without proving a ceiling over alternative learning lineages.

The mechanism worth testing is whether a learner can extract a reusable principle while discarding task-specific tactics. Compare raw experience, verified abstractions, deliberately mismatched lessons and no retained experience, with extraction and verification charged. Predict that matched abstractions help across the declared structural family and that harmful reuse increases when applicability conditions are violated. Improved internal experience revision is a possible remedy and belongs in the baseline.

Version differences matter for the stronger claim that a closed loop must deteriorate. The September revision of the RSI survey by Chen, Wang and Qu describes an unvanishing external-signal requirement. Zenil's August revision explicitly narrows that formulation: a per-generation correction fraction may vanish while cumulative correction remains sufficient. It distinguishes exact self-imitation, replacement, retention and correction, and does not assert universal collapse.

Zenil also distinguishes total information from the consequences an affordable procedure can make accessible. This is compatible with the role of computation in Definition 1.1: a new representation can expose a consequence without adding a hidden fact. Neither the information distinction nor the narrow resampling calculations show that an autonomous lineage lacks every useful representation change. A conceptual-discovery lower bound must constrain those alternatives explicitly.

The conditional transfer result separates three substantive obligations. First establish an affordably available contribution with independently meaningful structural quality. Then establish recipient interpretation, verification and acquisition within the remaining resources. Finally bound every admitted closed alternative, including internal analogy search, comparative archives, revised experience, task selection and changes across model generations. Existing studies motivate the first two and offer useful counterchecks to the third. They do not jointly prove the conjecture.

The central objective is to prove the separation. The developmental formulation in § 5.3 begins with absent experience and asks what family-specific argument makes every equally useful closed route expensive. An affordable qualified contributor and a recipient learning guarantee provide the constructive side; a necessary-event premise is insufficient unless its necessity and bound are derived for the admitted process.

Evidence can revise the setting while this proof is sought. A proved admitted procedure whose expected score exceeds the proposed ceiling invalidates that ceiling. One unusually successful run does not establish such an expectation, and failure of a tested menu does not establish a universal lower bound. Internal improvements belong in the closed process; a contribution the recipient cannot acquire leaves the constructive claim unproved. Fix the target, checker, endowments, resource limits and evaluation law before the decisive comparison.