Evolutionary Proof Search

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• AutoGraphForge: Towards Automated Graph Theory Discovery
• OEIS Open: How many conjectures can language models turn into theorems?
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving
• When Does Structured Knowledge Help Neural Theorem Proving?

Summary#

The mechanism inside DeepMind's full-featured AlphaProof Nexus agent (agent D), inspired by AlphaEvolve: prover subagents sample from and contribute to a shared population database of proof sketches, with an evolutionary loop driving the search. The hard problem it solves: evolutionary algorithms assume a graduated fitness landscape, but formal proof evaluation is binary (compiles / doesn't, complete / has sorry). The fix is to rate incomplete sketches by promise using LLM critics, turning a binary signal into a continuous fitness that an evolutionary search can climb.

This page now covers two independent answers to that problem. DeepMind's is above the substrate — an LLM judge invents the gradient. Meta AI/UVA's ProofEvolve (2026-08, ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving) derives it from the substrate: fitness is the fraction of the proof DAG the Lean kernel has already certified. Both keep the same outer shape (population/archive, variation operators, selection pressure); they differ in where the grading signal comes from and, consequently, in whether the search's own ranking can lie to it.

The binary-fitness problem#

A proof either type-checks sorry-free or it doesn't — there's no smooth gradient telling you a half-finished sketch is "closer." Evolutionary search needs such a gradient. AlphaProof Nexus bridges the gap by decoupling generation from fitness assignment: generate sketches freely, then assign fitness via relative LLM review of how promising each (often incomplete) sketch looks — its strategy clarity, the plausibility of remaining goals, and mathematical novelty.

Elo from LLM matches (Plackett–Luce + Gibbs)#

• Cheaper rater agents (Gemini 3.0 Flash) continuously sample sets of $P=7$ sketches and produce a relative ranking ($P=7$ balances information-per-call against context size).
• Outcomes are modeled with a Plackett–Luce distribution (each sketch has a latent strength $\lambda_s$), with a hierarchical Gamma prior for heavier tails while staying conjugate.
• Posterior strengths are inferred by Gibbs sampling ($I=1000$ samples, $B=200$ burn-in), converted to Elo: $\mathrm{Elo}s = 1200 + 400\log{10}\lambda_s^{\text{mean}}$.
• Sketch selection for matches uses Thompson sampling over the posterior; ties (raters sometimes output them) are broken by sampling from the model.

Evolutionary selection (P-UCB)#

Parent sketches for new episodes are chosen with a Predictor + Upper-Confidence-Bound (P-UCB) rule: filter to the top-64 by Elo, normalize to a base score $q\in[0,1]$, then $$\text{score}=q+c\frac{\sqrt{\sum V_i}}{v+1}$$ ($v$ = times this sketch was sampled, $c=0.2$ exploration constant). This exploits elite sketches while the UCB bonus explores newly-promoted ones, "preventing the search from collapsing into a single, suboptimal lineage." Diversity is further injected by stochastically prompting "decompose unsolved goals," "combine prior attempts," or "try a completely new approach" (the AlphaEvolve move).

Efficiency machinery#

• Global goal cache: every generated subgoal gets a deep hash of its exact Lean state (goal_id); if any prior sketch across the population already proved/disproved that state, the result (and its tactic/value) is retrieved instead of re-dispatched to AlphaProof. Novel subgoals are batched to AlphaProof over non-blocking RPCs.
• Budgets: each episode capped at 5 AlphaProof queries and 90 search-replace edits; AlphaProof itself bounded (~400 simulations, hard RPC timeout) to avoid stalling on intractable/hallucinated goals.
• Async controller: an asyncio event loop fans work across generation, validation, and Elo-rating threads; validation runs in Docker sandboxes (Lean v4.27 + Pantograph) and ends in SafeVerify (compiles, no sorryAx/axiom injection).

ProofEvolve: fitness read off the kernel instead of a judge#

ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving (Ye, Guan, Xie et al., UVA + Meta AI, arXiv 2608.26334, 2026-08-26, empirical) keeps the evolutionary shape and deletes the LLM critic. Its four pieces:

• Verified closure ρ as fitness. A proof attempt is a finite AND-OR proof DAG whose nodes are Lean tactic states and whose accepted hyperedges are kernel-checked realizers $F_e:\prod_i \mathrm{Prf}(s_i)\to\mathrm{Prf}(s)$. $\rho_D(s)$ is 1 for a closed node, 0 for an unexpanded frontier node, and otherwise the max over out-edges of the (uniformly) weighted mean of the children's values. So $\rho(D)\in[0,1]$, $\rho(D)=1\iff$ the root is closed, and ρ is monotone under extension. Every input to it is a kernel verdict: the grading signal cannot be wrong about what has been proved, only about how much the proved part is worth.
• A MAP-Elites archive instead of an Elo pool. Both systems cite Mouret & Clune (2015), but DeepMind uses it as a diversity intuition while ProofEvolve uses the actual algorithm: a descriptor $b(D)$ — binned depth, dominant tactic family, region of the schema index used — indexes one DAG per cell, a challenger evicts the incumbent only on strictly higher ρ, and parents are drawn softmax-over-ρ from occupied cells at temperature τ. Frontier scheduling then picks the open state $s$ maximizing $\Delta_D(s)=\rho^{[s\mapsto 1]}_D(r)-\rho_D(r)$ — the counterfactual structural gain from closing it.
• Three variation operators, all kernel-gated: decompose (introduce typed subgoals), repair (rewrite from the stored Lean error), recombine (instantiate a library schema). A rejected proposal writes its error into a store keyed by (target, DAG, state) and changes nothing else.
• A persistent schema library across problems. When an extension newly closes a node, kernel-checked extraction abstracts its free locals and used hypotheses into a prenex schema $\ell:\forall\mathbf{x},A_1\to\cdots\to A_m\to C$ with its proof term, and the library only grows ($\mathcal{L}t\subseteq\mathcal{L}{t+1}$). A later goal can be discharged by a typed substitution making $\mathrm{concl}(\ell)\sigma$ definitionally equal to it, with every undischarged premise re-exposed as a new subgoal and the whole application elaborated as one realizer. This is the piece AlphaProof Nexus has no analogue for: its global goal cache is keyed on an exact Lean state hash and so reuses only identical subgoals, and only within the run.

Theorem 1 / Corollary 1 formalize the obvious-but-necessary point: because every accepted edge and every library entry carries a checked realizer, no amount of evolutionary machinery can weaken soundness. The neural model decides only what to attempt.

What it measures#

• Main comparison (Table 1, reconciled cell-by-cell against pdftotext -layout and the §5.2 prose). All agentic systems reproduced by the authors on Claude Opus 4.8 under a matched per-target budget, mean of three runs: ProofEvolve 71.2 / 53.3 / 49.0 on PutnamBench / IMO-LeanProofBench / CombiBench, 57.8% average; LEAP 64.7 / 36.7 / 50.0 = 50.5; Hilbert 55.5 / 33.3 / 49.0 = 45.9; AxProver 37.1; Aristotle 32.8; ReAct 25.7. The same model under plain pass@16 sampling scores 0.0% on Putnam and 0.0% on IMO-Lean (10.0% on Combi, 3.3 average). The margin is concentrated on IMO-Lean (+16.6 points over LEAP); on CombiBench ProofEvolve is behind LEAP by one point.
• Operator ablation (§5.4 + Figure 3), 60 IMO-Lean problems, five seeds, budget held fixed. Full system solves 32/60 on average (22/30 Basic, 10/30 Advanced). Remove decomposition → 11 (9/2); remove recombination → 14 (11/3); remove repair → 9 (7/2). Every operator is load-bearing, and each one's contribution is larger on the Advanced split — but the run-to-run error bars on the ablated arms are wide (−repair spans roughly 11–36% on Basic in Figure 3) while the full system's are near-zero.
• Cross-problem inheritance, controlled (§5.6). On synthetic compositional lemma families where each target is built from earlier targets' lemmas: 19.8% solved with a growing library vs 7.3% with the library reset per target — 2.7×, everything else fixed.
• Cross-problem inheritance, real theorems (§5.6, Appendix F, Table 7). Lean Workbook re-verified down to 20,554 pairs, deduplicated to 10,968, split 1,000 eval / 9,968 source. Qwen3.5-397B-A17B-FP8 attempts every buildable source theorem once; its 5,546 kernel-accepted proofs are the library (57.9% self-solve over scoreable theorems). A five-judge Claude panel screens the eval set for residual near-duplicates and removes 256 (25.6%), leaving 744. At K=8 the library lifts solve rate 49.5% → 53.4% (+3.9 pp) while random retrieval from the same library gives +0.1 pp — the gain is selection, not more prompt examples. Of the 351 theorem-instances relevant retrieval closes that zero-shot leaves open, 322 (91.7%) reproduce no shown proof verbatim.
• Acceptance protocol (from AI-Driven Formal Proof Search, 2026-09-29 trim). A solve requires the proof to match the benchmark's ground-truth statement, carry no unresolved metavariables or placeholders, and pass the kernel; it is then independently re-verified, elaborated from scratch in a frozen Lean 4.29.1 / Mathlib 5e932f97 environment, with a restricted #print axioms check allowing only propext, Classical.choice and Quot.sound. native_decide is excluded outright because its code-generation path introduces an axiom outside the kernel. Across 400+ re-verifications: 0 false positives, and all 139 recorded solve events had a stored closing proof, with no reported ρ=1 lacking one.
• The leakage screen behind the 744 (from AI-Driven Formal Proof Search, 2026-09-29 trim). MinHash/LSH deduplication cut 2,362,946 candidate pairs to 10,968 representatives (a 46.6% reduction); five independent LLM judges then screened each of the 1,000 evaluation theorems against its 64 nearest library neighbours for restatements "up to renaming or a change of constants," removing 256 (25.6%) that had already survived alpha-equivalence and n-gram checks. Judge agreement was bimodal (73.0% unanimous; only 94 theorems in the decisive 2–3-flag band), and the threshold is consequential: three flags instead of two would have kept 801 rather than 744. The threshold is not validated.

The two findings that cut against the paper's own framing#

1. The library saturates almost immediately. Table 7's size sweep at K=8 reads +3.3 pp at 1,000 proofs, +2.6 at 2,000, +4.2 at 4,000, +3.9 at the full 5,546 — non-monotone, and every point inside roughly one run-to-run standard deviation of every other (Figure 5a's band confirms it visually). The depth sweep is the same shape: +3.9 / +4.6 / +3.4 / +5.3 at K = 8/16/32/64. So what the study actually demonstrates is that having about a thousand relevant verified proofs is worth ~4 points, not that accumulation compounds. For a paper whose thesis is "recursively self-improving agents that accumulate formal knowledge over time," the accumulation curve is flat after the first thousand entries. The controlled compositional-families result (2.7×) is the only place accumulation itself is shown to pay, and it is synthetic and built so that later targets require earlier lemmas.
2. The isolation that makes the library measurable also removes the evolution. §5.6 states it plainly: each condition is a single whole-proof attempt with no repair and no second sample, so "retrieved schemas act as in-context exemplars rather than as typed instantiations composed into a realizer; the DAG archive, decomposition, repair, and verified closure as a selection signal are all switched off." The +3.9 pp is therefore a measurement of RAG over verified Lean proofs, not of the typed recombination operator the method section defines. Nothing in the paper measures kernel-checked schema recombination in isolation at all.

What the two fitness designs imply about each other#

DeepMind's LLM critic can rank a sketch highly for strategy clarity and mathematical novelty — properties ρ cannot see, since ρ knows only which obligations the kernel has discharged. Conversely ρ cannot be wrong about progress, and it is free (it is computed from edges the kernel already checked, whereas the Elo pipeline runs a separate fleet of rater agents, $P=7$ sketches per call, Gibbs sampling at $I=1000$). ProofEvolve's result is that a system with no judge in the fitness loop at all beats five agentic baselines on the same model — which is evidence that the judge is not necessary, without being a measurement of how often the judge misleads. The honest reading: ρ dominates on cost and soundness; whether it dominates on search quality is untested, because no one has run the two fitness functions inside one system.

The control case: refutation, where the gradient is free#

Both designs above spend their ingenuity manufacturing a gradient over a binary verdict. The natural control is the mirror stage of the same discovery loop — searching for a counterexample rather than a proof — because there the objective is continuous for free. AutoGraphForge: Towards Automated Graph Theory Discovery (Pastorek, arXiv 2609.03478, empirical) runs exactly that. For a candidate inequality $f(G) \le R(g)(G)$ the margin is $f(G) - R(g)(G)$: positive exactly on a refuting graph, larger for a more decisive one, and defined on every object in the search space. No critic, no Elo, no proof DAG — every backend is simply a different way of maximising it. Six are implemented behind one margin interface: SMT encoding (z3), variable-neighbourhood search, linear cross-entropy over a per-edge probability matrix, UCT MCTS over edge add/delete actions, simulated annealing, and a deep-RL edge-selection policy in the Wagner/RLGT lineage.

So the refutation half gets, for nothing, the thing ρ and Elo both approximate. And the result is that it barely helps. Across five HPC partitions the entire six-algorithm battery contributed 1–22 counterexamples per round, while a precomputed static dataset of 348,207 graphs supplied 500–790 witnesses in round 1 of a single partition; in the single-pass baseline, 1,243 of 1,249 refutations came from datasets and random models, the remainder from active search. The author flags this himself as a single run with un-tuned default hyperparameters, not a verdict on the methods — which is the right caution. But it is a useful counterweight to both designs on this page: a free, well-shaped, continuous fitness does not by itself make evolutionary search the thing that finds the answer. What ProofEvolve demonstrates is that a kernel-derived gradient beats a judge-invented one; what this shows is that having a gradient at all is not the binding constraint on whether the search earns its keep. See Automated Conjecturing for the pipeline the margin interface sits in.

Where it sits#

Agent D combines this evolutionary search with the bespoke AlphaProof RL prover as a tool (AlphaProof Nexus). It's the most elaborate point on the A→D spectrum — and the one whose advantage the basic agent erased on most problems, retaining a 2×–5× cost edge only on the very hardest (Erdős #125, #138). So evolutionary proof search is best understood as the receding-frontier specialized scaffolding: it buys efficiency on the hardest problems today, with a diminishing margin as LLMs improve.

(Qualified 2026-09-21.) That "receding frontier" reading was drawn from a single post-hoc comparison on nine research problems at generous budget. ProofEvolve runs the comparison the other way — a whole competition benchmark, matched tight per-target budget (the 1× profile is 12 model calls, 60 Lean calls, 400K tokens, 1,800s wall-clock), frozen weights, same base model across arms — and there the elaborate scaffolding is worth 32 points of average solve rate over a plain ReAct loop (57.8% vs 25.7%) and the base model alone solves nothing at all on two of three benchmarks. Both readings are empirical; they are not in conflict once the budget regime is named. See Agentic Loops Overtake Bespoke Systems for the reconciliation.

The deeper difference is what persists. AlphaProof Nexus's population database and goal cache are per-run; its durable artifact is the AlphaProof network's weights, bought with a training cycle. ProofEvolve freezes every weight and makes the durable artifact an explicit, kernel-checked, human-readable schema library — the formal-math instance of the Knowledge-Centric Self-Improvement bet that the persistent object should be knowledge rather than the agent. Its advantage over the weight route is that a new result is available to the next problem immediately and carries a proof; its measured limit is that the library stops paying after roughly the first thousand entries.

(Third measurement, 2026-09-23 — and this one is on the machinery's own turf.) OEIS OPEN (OEIS Open: How many conjectures can language models turn into theorems?, Epoch AI, arXiv 2608.11941, empirical) re-runs the 492 open OEIS conjectures AlphaProof Nexus itself formalized and reported 44/492 (9%) on, under a hard $50-per-conjecture cap, using a ReAct loop with three tools and nothing else. Claude Opus 4.8 resolves 147 of 492 (30%), at an average $10 per resolved conjecture against the AlphaProof Nexus authors' own estimate of ~$10 (obtained by Epoch in personal correspondence, with up to ~$50 for their hardest few). So on this item set the elaborate search is 3.3× behind at matched cost per solve — not the "cost edge on the hardest problems" reading above, and not ProofEvolve's budget reconciliation either, since the budget is capped and the loop still wins.

What keeps it from settling the question is the same confound this machinery has had all along: the arms do not share a model. The prover subagents here are Gemini 3.1 Pro (19 February 2026); the loop runs Opus 4.8 and GPT-5.5 (28 May and 23 April). The result is therefore evidence for harness shrinkage across a model generation, not for search machinery being worthless at a fixed model — and the one experiment that would separate them, re-running agent D on a 2026-mid model, still has not been done. One detail does cut cleanly: a large share of the loop's solves are disproofs (37% on the full set, 43–48% on LITE), and refutation is precisely the regime where the control case below says the gradient is free and elaborate search stops paying.

Connections#

• Kernel-Level Proof Auditing — the retrospective justification for ProofEvolve's re-verification protocol: the restricted #print axioms check it adopted (whitelist propext/Classical.choice/Quot.sound, exclude native_decide) is exactly what separates a real proof from the 31–44% of one released prover's PutnamBench "successes" that compile cleanly and depend on sorryAx. ProofEvolve's 0 false positives across 400+ re-verifications is a number about a protocol nobody had yet shown was necessary

• Many-Agent Proof Harnesses — the population-search alternative that keeps the losers: Stellar Colosseum reduces candidates through an overlapping random-sample tree with each candidate's falsification report welded to it, synthesizing constructively rather than selecting, so a refuted branch contributes its refutation instead of dying. No fitness signal exists to select on, because nothing is kernel-checked

• Open-Ended Discovery Harnesses — the same anti-collapse goal with the heuristic replaced by a model. P-UCB, top-64 Elo filtering and the stochastic "try a completely new approach" prompt exist to stop the search "collapsing into a single, suboptimal lineage"; SwarmResearch hands that job to an LLM orchestrator choosing which git branch each new agent starts from. The claim is not yet settled — its own §3.5 reports the orchestrator's default behavior as near-greedy, which is the failure the hand-designed UCB bonus was built to make impossible

• AlphaProof Nexus — the full-featured agent (D) this mechanism powers

• AI-Driven Formal Proof Search — the paradigm; this is its most elaborate search strategy

• Automated Conjecturing — the upstream stage, and the control case above: the same discovery loop's refutation search, where a continuous margin fitness exists for free and the elaborate searchers still lose to a lookup table

• OEIS Open Benchmark — the third measurement and the machinery's worst showing: on the 492 OEIS conjectures AlphaProof Nexus itself formalized, a three-tool ReAct loop resolves 147 against its 44 at matched cost per solve, under a $50 cap — confounded by a two-generation model gap, and with 37–48% of the loop's solves being disproofs, the regime this page's control case already says elaborate search does not win

• Agentic Loops Overtake Bespoke Systems — the finding that the basic loop matched this machinery on most problems

• Client-Side Agent Optimization — population/budget/model-per-role (Flash raters, Pro provers) is the AgentOpt "combo" lever made concrete

• The Bitter Lesson — Elo/P-UCB/evolution is exactly the hand-engineered structure the bitter lesson predicts general methods will outrun

• Lean — the verifier whose binary signal forced the LLM-critic fitness workaround

• The Verifiability Thesis — rating incomplete sketches extends a verifiable domain's signal into the unverified-yet region

• LLM-as-a-Judge — the LLM-critic rater agents are an LLM-as-a-judge used as a fitness function: turning a binary verifier signal into a continuous grading gradient

• Knowledge-Centric Self-Improvement — ProofEvolve is the formal-math instance of that page's bet: weights frozen, agent generic, the only persistent object a curated knowledge artifact. It is also the strongest version of it, because Lean makes every library entry certified rather than merely distilled — and the one place the two corpora disagree is scale, where ProofEvolve's library-size sweep flattens after ~1,000 entries

• Tree Search over Agent Trajectories (LATS) — the closest relative outside formal math: the same UCB-family selection over a search tree, with an LLM judge plus a sample-frequency term standing in for this page's Elo and compiler fitness, and executed environment actions instead of proof sketches

Open Questions#

• The LLM-critic fitness is itself an unverified heuristic atop a verified substrate. How often does the Elo ranking mislead the search vs. the cost of computing it? Partially answered 2026-09-21 by ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving, and the partiality matters. ProofEvolve builds the same kind of search with the heuristic removed — fitness is verified closure ρ, computed for free from kernel-accepted edges, with no rater fleet, no Plackett–Luce posterior and no Gibbs sampling — and beats five agentic baselines on the same frozen base model at matched budget (57.8% average against LEAP's 50.5% and Hilbert's 45.9%). So the unverified ranking is demonstrably not necessary, and its compute is demonstrably avoidable. What remains unanswered is the question as literally posed: nobody has run LLM-critic Elo and verified closure as the only varied factor inside one system, so the misleading rate is still unmeasured, and ρ's own blind spot — it cannot see strategy clarity or novelty, only discharged obligations — is untested in the other direction. Note also that this is comparative evidence across two different provers, not a test of DeepMind's system.
• Hyperparameters ($c=0.2$, top-64, $P=7$) were "chosen empirically." How sensitive is the result to them, and do they transfer across mathematical domains? Partially answered 2026-09-21, on the transfer half only. ProofEvolve's per-benchmark margins over the same runner-up swing from +16.6 points on IMO-LeanProofBench to −1.0 on CombiBench, and its operator ablation splits the same benchmark by difficulty and finds every operator contributing roughly three times more on the Advanced split than the Basic one (full system 22/30 Basic vs 10/30 Advanced; without decomposition 9/30 and 2/30). So in this family of systems the configuration does not transfer uniformly across mathematical domains — combinatorics, where proofs rest on an explicit construction rather than an assembly of lemmas, is where the elaborate search stops paying. The sensitivity half is untouched: ProofEvolve reports no value for its own archive temperature τ or descriptor binning and runs no sweep over them, and the one hyperparameter it does sweep (retrieval depth K = 8/16/32/64) moves the outcome non-monotonically inside the noise band. Related evidence, 2026-09-29, When Does Structured Knowledge Help Neural Theorem Proving? (empirical; not an evolutionary system): a fixed context-augmentation configuration does not transfer across models either, since knowledge-graph context flips from +14 solves (Goedel-8B) to -14 (Qwen3-32B) on the same miniF2F set, with only per-problem selection recovering value. It says nothing about $c$, top-K or $P$ specifically, so the sensitivity half stays untouched.

Sources#

• Advancing Mathematics Research with AI-Driven Formal Proof Search
• ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving — ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving, Ye, Guan, Xie, Liu, Modi, Zhang, Wen, Kautz, Zhang (University of Virginia + Meta AI), arXiv 2608.26334, 2026-08-26, 28pp, empirical. Parse warning, in this wiki's convention: the raw is docling-derived and verify.py flagged table-collapse on 32 multi-value cells in Appendix Table 4 (mean kernel-verified transitions per budget). That flag is a false positive on the cells and a true positive on the header — the caption states entries are ordered seed 19 / seed 36 / seed 65, so 1.44/1.15/1.18 is a legitimate triple, but docling duplicated the budget column headers into nine columns (0.25× | 0.5× | 0.5× | 1× | 1× | 2× | 2× | 2× | 2×) for four real ones. Tables 1, 4, 5 and 7 were each re-read from pdftotext -layout on the local PDF and matched cell-for-cell against the prose before any number above was cited. All six figures were viewed: image_000000 is the Meta wordmark, not Figure 1 — the real Figure 1 is image_000001, which docling placed after the Figure 1 caption. The body carries an internal draft line "Date: August 10, 2026"; the arXiv date 2026-08-26 is authoritative
• AutoGraphForge: Towards Automated Graph Theory Discovery — arXiv 2609.03478, Ján Pastorek (Comenius University in Bratislava), 2026-09-03, 17pp, ITAT 2026 submission, empirical. Cited here only for §3.4.2 (the margin interface and the six counterexample-search backends) and §4.1's per-round witness attribution, both quoted from prose rather than from a table. Single author, workshop track, one run, un-tuned searcher hyperparameters — the "search algorithms barely contributed" observation is the author's own and he explicitly declines to generalize it; treat it as a datum, not a finding. Full source treatment on Automated Conjecturing
• OEIS Open: How many conjectures can language models turn into theorems? — Tom Adamczewski (Epoch AI), arXiv 2608.11941, 2026-08-12, 27pp, empirical. Cited here only for the 44/492-versus-147/492 comparison on the OEIS item set, the per-solve cost figures (including the AlphaProof Nexus authors' own estimate, obtained by correspondence and reported in the paper's footnote 9), the model-release dates that confound it, and the proof/disproof split read from Figure 1. It does not run agent D or any evolutionary search, so it is evidence about the item set and the loop, not a direct test of this page's machinery. Full treatment on OEIS Open Benchmark
• When Does Structured Knowledge Help Neural Theorem Proving? — Nabi, Vogl & Nabi (Stanford), arXiv 2609.34460, 2026-09-28, empirical. Cited only for one configuration-transfer datum (KG-context effect flips sign across models); no evolutionary search involved.