Pith. sign in

REVIEW 4 major objections 4 minor 39 references

A self-modifying Lean proof agent reaches 45.1% on held-out miniF2F by coevolving its benchmark.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-01 18:14 UTC pith:6JV3ALJZ

load-bearing objection A credible direction with a load-bearing comparison that is not yet established: the 45.1% vs 32.0% gap rests on best-of-9 vs best-of-2, an unspecified selection rule, and a single run. the 4 major comments →

arxiv 2607.17352 v1 pith:6JV3ALJZ submitted 2026-07-19 cs.AI cs.LGquant-ph

Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

Yuqing Li , Zeguan Wu , Yu Gan , Junyu Liu This is my paper
classification cs.AI cs.LGquant-ph
keywords Lean theorem provingself-evolving agentsbenchmark coevolutionformal verificationautomatic curriculumproof workflowscode-level self-improvement
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper argues that a theorem-proving agent need not be given a hand-designed proof workflow: it can evolve its own. The authors build a Lean agent whose workflow, prompts, and tools are fully mutable, while a small trusted runtime keeps every reported success anchored to Lean-verified proofs. Instead of evolving against a fixed benchmark, the agent's benchmark also coevolves, hardening only after the current champion has mastered easier tasks. On a held-out miniF2F test split, the best coevolving agent solves 45.1% of problems versus 32.0% for the best fixed-benchmark baseline and 12.7% for the seed. The result suggests that verifier-grounded self-evolution with a coevolving benchmark is a viable route to improving formal proof workflows.

Core claim

The central claim is that benchmark coevolution, not just agent self-modification, drives the improvement. The champion agent rewrites its own proof workflow and tools; then, if its raw solve rate clears a threshold, mastered tasks are retired from the active benchmark and replaced by laterally harder or next-level problems, with a single-anchor recalibration keeping normalized scores comparable as difficulty rises. Across 15 generations the held-out solve rate rises from 12.7% to 45.1%, while the best fixed-benchmark agent reaches 32.0%. All reported successes are re-verified under a trusted Lean snapshot, and the best evolved workflows turn out to be repair-centered rather than decompositi

What carries the argument

The load-bearing mechanism is a champion-driven, mastery-throttled curriculum update coupled to a single-anchor difficulty coefficient. Between generations, a small trusted runtime—which owns Lean verification, scoring, and benchmark management—evaluates the champion on the active benchmark; if the champion solves more than 30% of tasks, up to six tasks solved by every agent are retired and replaced, favouring domains with accumulated failures, and each replacement level is chosen by whether level-specific mastery exceeds 70%. A multiplicative recalibration re-runs the champion on the updated benchmark so the difficulty coefficient tracks accumulated hardening and normalized scores stay comp

Load-bearing premise

The headline gap rests on the assumption that the agents chosen for held-out evaluation—nine from the coevolving run, picked without a prespecified rule, and only the two highest-scoring fixed-benchmark agents, in a single run with no variance estimates—are representative enough that the difference reflects the method and not selection or noise.

What would settle it

Run the same 15-generation comparison under a pre-registered protocol: evaluate every accepted agent (or a random sample) on the held-out split, and repeat both conditions multiple times with different random seeds. If the coevolving advantage over the fixed-benchmark baseline shrinks to within run-to-run noise, or if a fixed-benchmark agent evaluated under the same protocol matches or exceeds 45.1%, the central claim would fail. A second check: confirm no held-out miniF2F test problem ever appears in the active benchmark or candidate pool.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Coevolving the benchmark with the agent keeps selection pressure near the agent's current frontier, avoiding both the weak signal of a too-hard benchmark and the saturation of a fixed easy one.
  • Agents can rediscover useful workflow structure on their own, such as verifier-feedback repair loops, lemma-name checking tools, and bounded node-level verification of sub-lemmas.
  • Decomposition-first workflows repeatedly appear in mutation traces but are usually pruned because the sparse pass/fail reward gives no credit for intermediate proof structure.
  • All improvements are grounded: since every solve is re-verified under a trusted Lean snapshot, a self-rewriting agent cannot count unverified claims as successes.
  • Longer runs or rewards that directly value verified decomposition are a natural next step the paper identifies for growing deeper proof graphs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the coevolution advantage holds across repeated runs, it suggests that static benchmarks undervalue self-improving agents by removing the adaptive difficulty signal that keeps evolution informative.
  • The same architecture could transfer to any formal verifier with a fixed correctness criterion; the difficulty-coefficient recalibration is a generic way to keep scores comparable as an environment self-hardens.
  • A testable extension: give selection pressure for verified intermediate nodes (or a small reward for node-level proof certificates) and measure whether deep, reusable proof graphs evolve instead of being competed away.
  • Because the held-out comparison selected agents after the fact, an immediate next experiment is to pre-register a sampling rule for trajectory agents and run multiple seeds; that would test whether the 45.1% versus 32.0% gap is robust.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper presents a self-modifying Lean proof agent in which a fixed trusted runtime wraps a mutable workspace containing the proof workflow, prompts, and tools. The agent is evolved over 15 generations while the active benchmark coevolves: the champion agent drives a mastery-throttled curriculum update that retires solved tasks and replaces them with laterally harder or next-level tasks, and a single-anchor recalibration updates a difficulty coefficient c so that normalized scores q = r·c are claimed to remain comparable across generations. Generalization is measured on a held-out miniF2F test split of 244 problems. The central claim is that the best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, supporting the conclusion that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark. The paper also reports a detailed lineage audit showing that repair-centered workflows dominate, that decomposition-based workflows repeatedly appear but are usually pruned, and that proof contexts remain mostly shallow.

Significance. The idea of coevolving the agent and its benchmark, rather than optimizing against a fixed external benchmark, is timely and relevant to the growing line of work on self-evolving LLM agents and formal theorem proving. The paper has several genuine strengths: the success criterion is grounded in Lean verification; the trusted-runtime/mutable-workspace separation is clearly described; the lineage record in Table 3 and the worked example in Appendix C provide unusual transparency about which proposed workflow changes actually survived selection; and Appendix A honestly discloses that the study is single-run with no variance estimates. If the headline quantitative comparison were robust, the paper would provide a useful proof-of-concept for a direction rather than a finished system. However, the central causal claim is currently supported only by an asymmetric, post hoc selection of evaluated agents from a single run. The 13-point gap between the coevolving and fixed-benchmark arms is therefore not established at the strength asserted in the abstract. The contribution is better viewed as a methodological proposal plus a preliminary trajectory, not a controlled comparison.

major comments (4)
  1. [§4.1, §4.2] The held-out comparison is not based on a pre-specified, symmetric evaluation rule. Section 4.1 states only that "we evaluate selected agents across the trajectory," and Section 4.2 states that for the fixed-benchmark baseline "we evaluate the two highest-scoring agents." Nine coevolving agents are evaluated (Table 1), but the rule for choosing those nine is not given. With no pre-registered selection rule, the 45.1% vs. 32.0% gap can be inflated by choosing favorable points from the non-monotonic coevolving trajectory. The authors should specify a rule in advance, or report held-out results for all accepted agents in both arms.
  2. [Appendix A] Appendix A states: "We report a single-run study; quantitative comparisons therefore come without variance estimates." Given the trajectory in Table 1 (12.7%, 38.9%, 29.9%, 11.9%, 25.4%, 40.6%, 25.4%, 45.1%), the held-out solve rate fluctuates widely. A single seed with no repeated runs cannot distinguish a genuine advantage of coevolution from run-to-run noise. At minimum, the paper should provide multiple seeds for both the coevolving and fixed-benchmark conditions, or clearly frame the result as a single observation rather than a comparative result.
  3. [§3.3, Eq. (1)] The single-anchor recalibration preserves the champion's normalized score by construction: c_{t+1} = c_t · r_t / max(r_{t+1}, ε), so q for the champion is unchanged. The text claims this places "an agent evaluated on a harder benchmark and one evaluated on an easier benchmark ... on a single scale." Matching the champion's score does not, by itself, make q comparable for non-champion agents, whose performance may change non-uniformly when the benchmark composition changes. The 'single scale' assertion is therefore an assumption rather than a consequence of the construction. The authors should state this explicitly and test sensitivity to the anchoring choice.
  4. [§4.2, Table 1] The headline comparison is best-of-selected (coevolving, 9 agents) versus best-of-two (fixed baseline). If the fixed-baseline arm had been given the same selection effort — e.g., evaluating 9 agents spread across its trajectory — the maximum could plausibly differ. The paper should report the full distribution of held-out scores for both arms, or match selection effort, before claiming that coevolution improves held-out solving.
minor comments (4)
  1. [Abstract] The abstract states "showing that verifier-grounded self-evolution can improve Lean proof workflows" without noting the single-run, post hoc evaluation limitations disclosed in Appendix A. Consider softening the wording or moving the caveats into the abstract.
  2. [Reproducibility] No code, data, or run artifacts are released, and the L1 pool is author-constructed. Without these, the lineage audit and the exact benchmark compositions cannot be independently checked.
  3. [Figure 1] The figure caption contains a typo: "Bechmark" should be "Benchmark." Also, the meaning of the illustrative equation 0.39×1 = 0.32×c is not explained in the caption until the body text.
  4. [Table 3] Table 3 is dense and uses many shorthand terms ("n/i", "part.", "trace invalid", "have-extraction"). Adding a short legend and defining all abbreviations in the caption would improve readability.

Circularity Check

3 steps flagged

Held-out comparison is not construction-circular, but the cross-generation selection score q = r·c is normalized by construction around the champion, and the champion-driven curriculum means the 'predicted' 45.1% vs 32.0% generalization gap rests on unmatched, post hoc selection with a single run.

specific steps
  1. self definitional [Section 3.3, Equation c_{t+1}=c_t·r_t/max(r_{t+1},ε); Section 3.4 q=r×c]
    "Because the benchmark hardens, raw solve rate is not comparable across generations. We restore comparability with a single-anchor recalibration: the champion is re-evaluated on the new benchmark and the difficulty coefficient is updated multiplicatively, c_{t+1}=c_t·r_t/max(r_{t+1},ε), c_0=1, where r_t is the champion's raw score on B_t, and the difficulty-normalized score reported for every agent is q=r×c. By construction the champion's normalized score is preserved across the recalibration (it is the anchor)"

    The normalized score q used for parent selection is not a new measurement of the champion: the definition of c guarantees q_champion(t+1)=q_champion(t) regardless of how the champion actually performs on the new benchmark. In the worked example the paper itself computes 0.39×1=0.32×c to solve for c, i.e., the champion's normalized score is set, not measured. For non-champion agents q is measured, but the champion's score — which is the reference point for the whole cross-generation scale — is an identity, not evidence.

  2. fitted input called prediction [Section 4.2; Table 1; Appendix A: "we evaluate the two highest-scoring fixed-benchmark agents..." and "we evaluate selected agents across the trajectory"]
    "For the fixed-benchmark baseline, where raw scores are measured on the same benchmark throughout, we evaluate the two highest-scoring agents on the held-out test split. For the coevolving run, where the active benchmark changes over time, we evaluate selected agents across the trajectory."

    The headline prediction — best coevolving agent 45.1% vs best fixed-benchmark agent 32.0% — is computed from 9 evaluated coevolving agents (Table 1) but only 2 fixed-benchmark agents, with no pre-specified rule for choosing the 9. Appendix A concedes: 'We report a single-run study; quantitative comparisons therefore come without variance estimates.' The 13-point gap is therefore not a predicted quantity of the method; it is an artifact of the evaluation protocol, since best-of-9 vs best-of-2 post hoc selection makes the comparison statistically forced.

  3. other [Section 3.3 and Algorithm 1, lines 6-28; Figure 1 caption]
    "Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update ... the updated benchmark is then used to evaluate the next generation."

    The agent under evaluation is always evaluated on a benchmark that the agent's own champion just constructed: replacements are 'domain-matched' to the archive's failures and harder tasks are inserted only when the champion's mastery threshold is met. So the 'evolutionary signal' being optimized is a self-selected curriculum, and holdout generalization is not directly predicted by it. This is a design limitation distinct from the constructed q-identity, but it means the coevolutionary run and the fixed benchmark are not measured with comparable measurement effort.

full rationale

The core of this paper is NOT circular in the classic sense: all reported proof solves are grounded in a trusted Lean verifier, the seed is deliberately minimal, and the held-out miniF2F result (45.1% vs 32.0%) is an external, fixed benchmark never touched by evolution. There is no self-definitional collapse of the final capability claim into its inputs, because the final evaluation is on a fixed external test split. However, two internal links in the derivation chain are partially circular by construction. First, the cross-generation selection score q=r·c: the recalibration equation c_{t+1}=c_t·r_t/max(r_{t+1},ε) makes the champion's normalized score an identity (c updated exactly to preserve q), so the 'difficulty coefficient' is not an independently measured comparison scale but a fitted parameter anchored to the champion. Second, the headline comparison is statistically forced at the evaluation level: 9 trajectory agents vs 2 fixed-benchmark agents, chosen post hoc with no pre-specified rule, and explicitly a single run with no variance estimates. That does not make the held-out solves fake, but it makes the claimed 13-point improvement a best-of-9 vs best-of-2 artifact rather than a fair prediction. No load-bearing self-citation was found; citations to DGM/RQGM/POET are context-setting, not justifications. Score 5 reflects: the final held-out claim is externally grounded, but the two central comparisons/method are partially circular by construction.

Axiom & Free-Parameter Ledger

7 free parameters · 5 axioms · 3 invented entities

The paper introduces several hand-set thresholds and a private task pool that jointly determine the coevolution trajectory. The difficulty coefficient c is self-anchored to the champion's raw scores, and the L1 curriculum tasks are not public, so the exact evolutionary dynamics cannot be independently reconstructed. The held-out miniF2F split is the one externally grounded benchmark in the loop.

free parameters (7)
  • γ (benchmark update threshold) = 0.30
    Champion must exceed 0.30 raw solve rate to trigger a benchmark update; hand-set, controls how often the curriculum hardens.
  • τ (graduation mastery threshold) = 0.70
    Level-specific solve rate needed to replace a retired task with one from the next-harder level; hand-set in Section 3.3 / Algorithm 1.
  • κ (max retired tasks per generation) = 6
    Upper bound on curriculum replacement per generation; hand-set, with κ=0 for the fixed-benchmark baseline.
  • ε (recalibration floor) = 0.1
    Floor in c_{t+1}=c_t·r_t/max(r_{t+1},ε); hand-set, prevents division blowup and shapes difficulty-coefficient growth.
  • Initial active benchmark composition L1:L2:L3 = 27:46:3 of 76 tasks
    Chosen so the seed solves ≈37% overall (28/76), preserving an informative evolutionary signal; hand-picked starting distribution.
  • c_0 (initial difficulty coefficient) = 1.00
    Origin of the normalized-score scale; arbitrary normalization anchor.
  • Candidate pool sizes per level = 52 L1, 57 L2, 256 L3
    Task pool from which replacements are drawn; limits curriculum diversity and is chosen by authors.
axioms (5)
  • domain assumption Lean 4 v4.30.0 with Mathlib, under a trusted snapshot, soundly distinguishes valid from invalid proofs and cannot be tampered with by the mutable agent.
    Everything labeled 'solved' is only as trustworthy as the Lean kernel and the runtime protections described in Section 3.2 Part B; no independent formal proof of the runtime's isolation is given.
  • domain assumption The held-out miniF2F test split (244 problems) is a fair generalization measure, disjoint from the active benchmark's L2 valid split.
    Stated in Section 4 / Appendix A; no leakage analysis or test-set contamination check is provided.
  • domain assumption Temperature-0 DeepSeek outputs are stable enough that single-run differences are meaningful; the authors note non-negligible output instability on boundary problems.
    Appendix A; the instability caveat weakens all quantitative comparisons, which rely on one run each.
  • ad hoc to paper Normalized scores q = r·c remain comparable across generations even though c is anchored to the champion's own raw scores.
    Section 3.3: by construction the champion's normalized score is preserved across recalibration; this makes q an internally defined scale rather than an externally validated one.
  • domain assumption The author-constructed L1 tasks and the three-level stratification provide the intended difficulty gradient (seed rates ≈0.52/0.18/0.00).
    Appendix A; L1 tasks are not released, so the gradient and curriculum are not externally checkable.
invented entities (3)
  • Difficulty coefficient c_t no independent evidence
    purpose: Normalize scores across benchmarks of changing difficulty and weight parent selection
    Defined by the single-anchor update c_{t+1}=c_t·r_t/max(r_{t+1},ε) (Section 3.3); its values (1.00→3.17) are computed from the champion's own solve rates, with no external anchor.
  • Mastery-throttled curriculum update no independent evidence
    purpose: Retire mastered active-benchmark tasks and replace them laterally or with harder tasks
    An algorithm specified by the authors (Algorithm 1) with hand-set thresholds γ, τ, κ, ε; no independent validation of the update rule alone.
  • Author-constructed L1 warm-up lemma pool no independent evidence
    purpose: Easy curriculum rung that the seed can solve ~52% of, providing initial selection signal
    52 private tasks not released; they are central to the coevolution trajectory but externally unverifiable.

pith-pipeline@v1.3.0-alltime-deepseek · 17257 in / 18086 out tokens · 171672 ms · 2026-08-01T18:14:25.921807+00:00 · methodology

0 comments
read the original abstract

Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.

Figures

Figures reproduced from arXiv: 2607.17352 by Junyu Liu, Yu Gan, Yuqing Li, Zeguan Wu.

Figure 1
Figure 1. Figure 1: Champion-driven agent–benchmark coevolution. A seed agent produces first￾generation (G1) children that stream into a shared archive as they are evaluated, so a strong early child can already parent later siblings in the same generation; the strongest child becomes the champion, seeds the next generation (G2), and also drives the benchmark update. Evaluation records from all agents are collected. The benchm… view at source ↗
Figure 2
Figure 2. Figure 2: Evolution tree for the accepted lineage. Bold nodes mark agents with decomposition [PITH_FULL_IMAGE:figures/full_fig_p015_2.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

39 extracted references · 29 linked inside Pith

  1. [1]

    Benjamin S. Bloom. Learning for mastery.Evaluation Comment, 1(2):1–12, 1968

    1968

  2. [2]

    Brant and Kenneth O

    Jonathan C. Brant and Kenneth O. Stanley. Minimal criterion coevolution: A new approach to open-ended search. InProceedings of the Genetic and Evolutionary Computation Conference, pages 67–74, 2017

    2017

  3. [3]

    Karlsson, Jie Fu, and Yemin Shi

    Guangyao Chen, Siwei Dong, Yu Shu, Ge Zhang, Jaward Sesay, Börje F. Karlsson, Jie Fu, and Yemin Shi. Autoagents: A framework for automatic agent generation. InProceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI), 2024. arXiv:2309.17288

    Pith/arXiv arXiv 2024

  4. [4]

    Multi-agent evolve: Llm self-improve through co-evolution.arXiv preprint arXiv:2510.23595, 2025

    Yixing Chen, Yiding Wang, Siqi Zhu, Haofei Yu, Tao Feng, Muhan Zhang, Mostofa Patwary, and Jiaxuan You. Multi-agent evolve: Llm self-improve through co-evolution.arXiv preprint arXiv:2510.23595, 2025

    arXiv 2025

  5. [5]

    Fowl, and Sanjeev Arora

    Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H. Fowl, and Sanjeev Arora. Goedel-architect: Streamlining formal theorem proving with blueprint generation and refinement.arXiv preprint arXiv:2606.06468, 2026

    Pith/arXiv arXiv 2026

  6. [6]

    Emergent complexity and zero-shot transfer via unsupervised en- vironment design

    Michael Dennis, Natasha Jaques, Eugene Vinitsky, Alexandre Bayen, Stuart Russell, Andrew Critch, and Sergey Levine. Emergent complexity and zero-shot transfer via unsupervised en- vironment design. InAdvances in Neural Information Processing Systems (NeurIPS), 2020. arXiv:2012.02096

    Pith/arXiv arXiv 2020

  7. [7]

    Promptbreeder: Self-referential self-improvement via prompt evolution.arXiv preprint arXiv:2309.16797, 2023

    Chrisantha Fernando, Dylan Banarse, Henryk Michalewski, Simon Osindero, and Tim Rock- täschel. Promptbreeder: Self-referential self-improvement via prompt evolution.arXiv preprint arXiv:2309.16797, 2023

    Pith/arXiv arXiv 2023

  8. [8]

    A survey of self-evolving agents: What, when, how, and where to evolve on the path to artificial super intelligence.Transactions on Machine Learning Research, 2026

    Huan-ang Gao, Jiayi Geng, Wenyue Hua, Mengkang Hu, Xinzhe Juan, Hongzhang Liu, Shilong Liu, Jiahao Qiu, Xuan Qi, Yiran Wu, Hongru Wang, Han Xiao, Yuhang Zhou, Shaokun Zhang, Jiayi Zhang, Jinyu Xiang, Yixiong Fang, Qiwen Zhao, Dongrui Liu, Qihan Ren, Cheng Qian, Zhenhailong Wang, Minda Hu, Huazheng Wang, Qingyun Wu, Heng Ji, and Mengdi Wang. A survey of se...

    Pith/arXiv arXiv 2026

  9. [9]

    Genenv: Difficulty-aligned co-evolution between llm agents and environment simulators.arXiv preprint arXiv:2512.19682, 2025

    Jiacheng Guo, Ling Yang, Peter Chen, Qixin Xiao, Yinjie Wang, Xinzhe Juan, Jiahao Qiu, Ke Shen, and Mengdi Wang. Genenv: Difficulty-aligned co-evolution between llm agents and environment simulators.arXiv preprint arXiv:2512.19682, 2025

    arXiv 2025

  10. [10]

    Automated design of agentic systems.arXiv preprint arXiv:2408.08435, 2024

    Shengran Hu, Cong Lu, and Jeff Clune. Automated design of agentic systems.arXiv preprint arXiv:2408.08435, 2024

    Pith/arXiv arXiv 2024

  11. [11]

    Yukun Huang, Leonardo F. R. Ribeiro, Momchil Hardalov, Bhuwan Dhingra, Markus Dreyer, and Venkatesh Saligrama. Deepfact: Co-evolving benchmarks and agents for deep research factuality.arXiv preprint arXiv:2603.05912, 2026. Accepted at ACL 2026. 19

    Pith/arXiv arXiv 2026

  12. [12]

    Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al

    Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, Yannick Schroecker, Hussain Masoom, et al. Olympiad- level formal mathematical reasoning with reinforcement learning.Nature, 651:607–613, 2026. Published online 2025

    2026

  13. [13]

    Shen, Daniel Burkhardt, Meghdad Kurmanji, Nurbek Tastan, LorenzoSani, NiccolòAlbertoEliaVenanzi, AmbroiseOdonnat, ZeyuCao, BillMarino, Xinchi Qiu, and Nicholas D

    Alex Iacob, Andrej Jovanović, William F. Shen, Daniel Burkhardt, Meghdad Kurmanji, Nurbek Tastan, LorenzoSani, NiccolòAlbertoEliaVenanzi, AmbroiseOdonnat, ZeyuCao, BillMarino, Xinchi Qiu, and Nicholas D. Lane. The red queen gödel machine: Co-evolving agents and their evaluators.arXiv preprint arXiv:2606.26294, 2026

    Pith/arXiv arXiv 2026

  14. [14]

    Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. InInternational Conference on Learning Repre- sentations, 2023. arXiv:2210.12283

    Pith/arXiv arXiv 2023

  15. [15]

    Le, Burak Gokturk, Thang Luong, Tomas Pfister, and Nanyun Peng

    Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Olšák, Edward Lockhart, Quoc V. Le, Burak Gokturk, Thang Luong, Tomas Pfister, and Nanyun Peng. Leap: Supercharging llms for formal mathematics with agentic frameworks. arXiv preprint arXiv:2606.03303, 2026

    Pith/arXiv arXiv 2026

  16. [16]

    Goedel-prover- v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.arXiv preprint arXiv:2508.03613, 2025

    Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, Jiayun Wu, Jiri Gesi, Ximing Lu, David Acuna, Kaiyu Yang, Hongzhou Lin, Yejin Choi, Danqi Chen, Sanjeev Arora, and Chi Jin. Goedel-prover- v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction.arXiv prepri...

    Pith/arXiv arXiv 2025

  17. [17]

    Alexander Novikov, Ngân V˜ u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. Alphaevolve: A coding agent for scien- tific and al...

    Pith/arXiv arXiv 2025

  18. [18]

    Generative language modeling for automated theorem prov- ing.arXiv preprint arXiv:2009.03393, 2020

    Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem prov- ing.arXiv preprint arXiv:2009.03393, 2020

    Pith/arXiv arXiv 2009

  19. [19]

    Auto- matic curriculum learning for deep rl: A short survey

    Rémy Portelas, Cédric Colas, Lilian Weng, Katja Hofmann, and Pierre-Yves Oudeyer. Auto- matic curriculum learning for deep rl: A short survey. InInternational Joint Conference on Artificial Intelligence (IJCAI), 2020. arXiv:2003.04664

    Pith/arXiv arXiv 2020

  20. [20]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.arXiv preprint arXiv...

    Pith/arXiv arXiv 2025

  21. [21]

    A self-improving coding agent

    Maxime Robeyns, Martin Szummer, and Laurence Aitchison. A self-improving coding agent. arXiv preprint arXiv:2504.15228, 2025

    Pith/arXiv arXiv 2025

  22. [22]

    Pawan Kumar, Emilien Dupont, Francisco J

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathematical discoveries from program search with large language models.Nature, 625:468–475, 2024. 20

    2024

  23. [23]

    Gödel machines: Fully self-referential optimal universal self-improvers

    Jürgen Schmidhuber. Gödel machines: Fully self-referential optimal universal self-improvers. In Ben Goertzel and Cassio Pennachin, editors,Artificial General Intelligence, Cognitive Tech- nologies, pages 199–226. Springer, 2007

    2007

  24. [24]

    Agentsquare: Automatic llm agent search in modular design space

    Yu Shang, Yu Li, Keyu Zhao, Likai Ma, Jiahe Liu, Fengli Xu, and Yong Li. Agentsquare: Automatic llm agent search in modular design space. InInternational Conference on Learning Representations, 2025. arXiv:2410.06153

    Pith/arXiv arXiv 2025

  25. [25]

    Lean copilot: Large language models as copilots for theorem proving in lean

    Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving in lean. InInternational Conference on Neuro-symbolic Systems (NeuS), 2025. arXiv:2404.12534

    Pith/arXiv arXiv 2025

  26. [26]

    A survey on self-evolution of large language models

    Zhengwei Tao, Ting-En Lin, Xiancai Chen, Hangyu Li, Yuchuan Wu, Yongbin Li, Zhi Jin, Fei Huang, Dacheng Tao, and Jingren Zhou. A survey on self-evolution of large language models. arXiv preprint arXiv:2404.14387, 2024

    Pith/arXiv arXiv 2024

  27. [27]

    Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition

    George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition. InAdvances in Neural Information Processing Systems (NeurIPS) Datasets and Benchmarks, 2024. arXiv:2407.11214

    Pith/arXiv arXiv 2024

  28. [28]

    Vygotsky.Mind in Society: The Development of Higher Psychological Processes

    Lev S. Vygotsky.Mind in Society: The Development of Higher Psychological Processes. Harvard University Press, 1978. Edited by Michael Cole, Vera John-Steiner, Sylvia Scribner, and Ellen Souberman

    1978

  29. [29]

    Rui Wang, Joel Lehman, Jeff Clune, and Kenneth O. Stanley. Paired open-ended trailblazer (poet): Endlessly generating increasingly complex and diverse learning environments and their solutions.arXiv preprint arXiv:1901.01753, 2019

    Pith/arXiv arXiv 1901

  30. [30]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval- augmented language models. InAdvances in Neural Information Processing Systems (NeurIPS) Datasets and Benchmarks, 2023. arXiv:2306.15626

    Pith/arXiv arXiv 2023

  31. [31]

    Ruiyi Yang, Zechen Li, Hao Xue, Imran Razzak, and Flora D. Salim. Mage: Multi-agent self-evolution with co-evolutionary knowledge graphs.arXiv preprint arXiv:2605.10064, 2026

    Pith/arXiv arXiv 2026

  32. [32]

    Gödel agent: A self-referential agent framework for recursively self-improvement

    Xunjian Yin, Xinyi Wang, Liangming Pan, Li Lin, Xiaojun Wan, and William Yang Wang. Gödel agent: A self-referential agent framework for recursively self-improvement. InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 27890–27913, Vienna, Austria, 2025. Association for Computational Ling...

    Pith/arXiv arXiv 2025

  33. [33]

    Evoagent: Towards automatic multi-agent generation via evolutionary algorithms

    Siyu Yuan, Kaitao Song, Jiangjie Chen, Xu Tan, Dongsheng Li, and Deqing Yang. Evoagent: Towards automatic multi-agent generation via evolutionary algorithms. InAnnual Confer- ence of the Nations of the Americas Chapter of the Association for Computational Linguistics (NAACL), 2025. arXiv:2406.14228

    Pith/arXiv arXiv 2025

  34. [34]

    Self-taught opti- mizer (stop): Recursively self-improving code generation

    Eric Zelikman, Eliana Lorch, Lester Mackey, and Adam Tauman Kalai. Self-taught opti- mizer (stop): Recursively self-improving code generation. InConference on Language Modeling (COLM), 2024. arXiv:2310.02304. 21

    Pith/arXiv arXiv 2024

  35. [35]

    Darwin gödel machine: Open-ended evolution of self-improving agents.arXiv preprint arXiv:2505.22954, 2025

    Jenny Zhang, Shengran Hu, Cong Lu, Robert Lange, and Jeff Clune. Darwin gödel machine: Open-ended evolution of self-improving agents.arXiv preprint arXiv:2505.22954, 2025

    Pith/arXiv arXiv 2025

  36. [36]

    Hyperagents.arXiv preprint arXiv:2603.19461, 2026

    Jenny Zhang, Bingchen Zhao, Wannan Yang, Jakob Foerster, Jeff Clune, Minqi Jiang, Sam Devlin, and Tatiana Shavrina. Hyperagents.arXiv preprint arXiv:2603.19461, 2026

    arXiv 2026

  37. [37]

    Aflow: Automating agentic workflow generation

    Jiayi Zhang, Jinyu Xiang, Zhaoyang Yu, Fengwei Teng, Xionghui Chen, Jiaqi Chen, Mingchen Zhuge, XinCheng, SiruiHong, JinlinWang, BingnanZheng, BangLiu, YuyuLuo, andChenglin Wu. Aflow: Automating agentic workflow generation. InInternational Conference on Learning Representations, 2025. arXiv:2410.10762

    Pith/arXiv arXiv 2025

  38. [38]

    Minif2f: A cross-system benchmark for formal olympiad-level mathematics

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: A cross-system benchmark for formal olympiad-level mathematics. InInternational Conference on Learning Representations,

  39. [2022]

    arXiv:2109.00110. 22

    Pith/arXiv arXiv