\section{Experiments}\label{sec:experiments}

Every experiment of this section fixes its measured quantity before the runs, compares each arm with controls that spend the same kind of budget, and counts a step only after the check that the run itself performs. The unit of cost is one check of one closed composite. The experiments are, in order: a router of strategies on the two Millennium benchmarks; the crossing network on Erd\H{o}s problem 1183, where the only advance came from a change of representation; the crossing network on Yang--Mills and Hodge, where it reaches the range $\beta_{W}<\frac13$; the booster layer; the memory, the channel and the agents; and the barrier and pattern matrix.

\subsection{A router of strategies on Hodge and Yang--Mills}\label{ssec:router}

In its first form the package represented each of the two open problems as a tree whose root is the statement and whose leaves are the pieces it splits into: a faithful Lean statement, the lattice gap at strong coupling, fine-scale control at weak coupling, the crossover window at order-one coupling with two attempts on it, and the continuum limit for Yang--Mills; a faithful Lean statement, (F2) in dimension at most five, for CM abelian varieties, for split Weil eightfolds and through a semiregular object on $E_{0}^{6}$, and (F3$'$) for the square of a K3 surface with real multiplication and for Fermat fourfolds for Hodge. A run picks a leaf and one of eight moves (reduction, special case and lift, certificate, construction, counterexample, flow with surgery, descent, physics first), and a move is accepted only when a computation of the package checks it. These are the trees of six and eight leaves on which the router was run; Section~\ref{ssec:headline} adds the leaves the crossing network opened. Five policies choose the move: uniformly; by the prior of the Lean-formalised manuscripts of \cite{OAI26b}; by a router that averages that prior with the share of the settled Erd\H{o}s problems solved by each move and is reinforced by accepted steps; by the profile of a local language model, the softmax of the next-token logits of a model with $1.5\times10^{9}$ parameters over the letters of the eight moves \cite{Qwe24}; and by the mixture of the last two with weight $\frac12$.

Over $200$ seeds of $12$ rounds every policy finds the same two accepted steps, the reduction of the Hodge conjecture for a Fermat fourfold of degree $m$ to the degrees with leftover characters, by Shioda's criterion for zero-sum pairs and triples, and the strong-coupling gap $m\ge-\log(9\beta_{W}/2)$ for $\beta_{W}<\frac29$. The mean number of attempts before both are found is $36.3$ for the uniform policy, $38.3$ for the corpus prior, $35.4$ for the router, $26.3$ for the profile of the model and $33.5$ for the mixture; of $65$ to $67$ attempts per run, between $50.9$ and $52.9$ go to moves that have no checkable formulation at their leaf. The model's profile is the best of the five, by a factor of $1.38$ over the uniform policy, and no policy moves any open leaf. Both accepted steps are results of \cite{BB26c,BB26d}; the benchmark measures how fast a policy finds a step that a computation can check, and on these trees the only such steps are known ones. Moving a leaf needed a different proposer, one that combines known constructions instead of choosing among moves, and that is the crossing network of the next subsection.


\input{sections/sec10d_crossing}
\input{sections/sec10c_headline}
\input{sections/sec10e_memory}