Pith. sign in

REVIEW 3 major objections 5 minor 53 references

A multi-agent LLM system with a tripartite harness can co-pilot full-cycle mathematical research and has solved eleven open problems.

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 · grok-4.5

2026-07-11 19:28 UTC pith:AYAUAYJA

load-bearing objection Solid multi-agent harness with real Lean case studies and open-problem traces; the '11 solved' headline cannot be scored independently of same-team human work. the 3 major comments →

arxiv 2607.04394 v1 pith:AYAUAYJA submitted 2026-07-05 cs.AI cs.SC

MechMath Agent Team: LLM Driven Agents for Mathematical Research

Yichuan Cao , Ruichen Qiu , Junqi Liu , Jiaqi Wang , Dakai Guo , Ruyong Feng , Lihong Zhi , Xiao-Shan Gao This is my paper
classification cs.AI cs.SC MSC 68T2068T5003B35
keywords multi-agent systemslarge language modelsmathematical reasoningformal verificationLean 4theorem provingknowledge baseharness architecture
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.

Mathematical research resists ordinary LLM pipelines because its paths are non-linear, its standards are absolute, and its timelines are long. This paper introduces MechMath Agent Team (MMAT), an LLM-driven multi-agent co-pilot built on a Harness Architecture that cleanly separates control, execution, and augmentation. Three specialized agents—a knowledge-base manager, a natural-language prover, and a Lean-4 formal prover—run in a closed loop that turns informal exploration into machine-checked proofs. Over a two-month internal deployment the system was applied to open problems in number theory, algebraic complexity, differential algebra, operator algebra, and inequalities and is reported to have solved eleven of them. A sympathetic reader cares because the work claims that structured multi-agent collaboration, formal verification, and human breakpoints together can move AI reasoning from static benchmarks into actual research assistance.

Core claim

The authors claim that a decoupled Harness Architecture—Control, Execution, and Augmentation planes—lets specialized LLM agents (Knowledge Base Manager, Natural Language Prover, Formal Language Prover) operate in a closed loop and produce formally certified mathematical proofs, thereby serving as a co-pilot across the full research cycle; they report solving eleven open problems over a two-month deployment as empirical support.

What carries the argument

The Harness Architecture: a tripartite scaffold that places global scheduling in a Control Plane (orchestrator, execution DAG, task ledger), isolates agents in an Execution Plane (sandboxed workspaces and file-based handoffs), and extends cognition in an Augmentation Plane (human–AI breakpoints and stratified continual memory of negative constraints). This separation is what lets open-ended exploration coexist with deterministic state and Lean-4 certification.

Load-bearing premise

That the eleven solved problems, many appearing in companion papers co-authored by the same team with mixed human involvement, count as independent evidence of the agent architecture rather than joint human–AI work whose automation share is not measured.

What would settle it

An independent re-run of the same open problems with the released agent stack that fails to recover the reported natural-language or Lean proofs without large additional human rewriting, or an audit showing that critical Lean developments rest on unreduced axioms beyond those the paper discloses.

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

If this is right

  • Multi-agent systems can audit existing proof chains, isolate logical flaws, and produce counterexamples at extreme scales.
  • Natural-language discovery can be closed into Lean-4 certificates through iterative formalize–feedback loops.
  • Object-oriented knowledge cards (partial proofs, obstructions, Lean artifacts) can accumulate reusable research memory across sessions.
  • A single problem can be steered into a multi-problem project (e.g., sparse-polynomial multiplication, divisibility, GCD, factorization).
  • Human mathematicians can inject strategic corrections at structured breakpoints without restarting the entire search.

Where Pith is reading between the lines

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

  • The same isolation-and-handoff pattern could transfer to other high-stakes domains that need exploratory error contained (formal software verification, protocol design).
  • Publishing quantified human-vs-agent contribution ratios would let outsiders test how much of the co-pilot claim is automation versus collaboration.
  • Shared libraries of distilled negative constraints might reduce repeated failure modes across independent research groups.
  • Closed-loop NL-to-Lean formalization could lower the barrier for mathematicians who do not write interactive theorem-prover code by hand.

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

3 major / 5 minor

Summary. The paper introduces MechMath Agent Team (MMAT), an LLM-driven multi-agent system intended as a co-pilot for the full cycle of mathematical research. It proposes a tripartite Harness Architecture that separates Control (orchestrator with execution graph and task ledger), Execution (isolated workspaces and file-based handoffs), and Augmentation (human–AI co-reasoning and stratified memory) planes. This is instantiated as three agents—KB-Manager, NL-Prover, and FL-Prover (Lean 4)—operating in a closed Inform–Formalize–Feedback–Archive loop. Empirical claims rest on a two-month deployment that purportedly solved 11 open problems across number theory, algebraic complexity, differential algebra, operator algebra, and inequalities (Table 4), illustrated by three case studies: a full natural-to-formal pipeline for OEIS A287616 (§4.1), orchestrated certification of 40 320 cones for Vasc’s n=9 inequality (§4.2), and a sparse-polynomial project that includes proof-chain auditing, a large-scale counterexample, and human–AI reconstruction (§4.3).

Significance. If the architecture and co-pilot claims hold, the work is significant for AI-assisted mathematical research: it moves beyond static benchmarks to open problems, couples natural-language exploration with Lean 4 mechanical verification, and documents concrete agent traces (e.g., 137 subagents and ~3500 lines of Lean for A287616; parallel branches and exception handling for the 40 320-cone certification; counterexample construction at N=10^20). The Harness design (deterministic state structures, sandbox isolation, file handoffs, negative-constraint memory) is a concrete engineering contribution that could be reused. Machine-checked fragments and reproducible computational certificates are genuine strengths. The significance is tempered by the fact that nearly all empirical successes are reported only via same-team companion arXiv preprints, so the incremental value of the multi-agent harness versus skilled human mathematicians using ordinary LLM tools remains hard to isolate from this manuscript alone.

major comments (3)
  1. [Abstract; Table 4; §4] The central empirical claim (Abstract; Table 4; §4) that MMAT “solved 11 problems” and thereby demonstrated co-pilot capacity throughout the research cycle rests almost exclusively on companion arXiv preprints co-authored by the same team (refs. [6–8,14,15,19,20,36,51] etc.). Table 4’s Human column marks human participation for most entries, yet the manuscript supplies no counts of intervention breakpoints (§2.3.1), fraction of novel lemmas/routes supplied by humans versus agents, or task-ledger excerpts that would let a reader separate MMAT-driven discovery from human-led research assisted by LLM tools. Without such quantification or public execution logs, the load-bearing co-pilot claim cannot be independently assessed from this paper.
  2. [§4.3; Figure 7] §4.3.1–4.3.2 present the sparse-polynomial audit and reconstruction as evidence of autonomous proof-chain auditing and bidirectional co-reasoning, including a counterexample at N=10^20 that falsifies a prior probabilistic claim. These are valuable case studies, but the manuscript does not isolate the necessity of the Harness Architecture (execution graph, task ledger, isolated workspaces) via ablation or comparison against a simpler single-agent or non-harness baseline. Consequently it remains unclear whether the reported successes require the tripartite design or would arise from ordinary LLM + Lean + human interaction.
  3. [Table 4; §4.1; Figure 3] The paper asserts a closed-loop, formally certified pipeline (Figure 3; §3), yet Table 4 shows that only a minority of the 11 results are fully formalized (✓); several are partial (◆, axioms retained) or unformalized (✗). For the flagship A287616 case (§4.1) the FL-Prover still leaves the computational cover certificate and a classical genus theorem as axioms. The claim that the system “produce[s] formally certified mathematical proofs” therefore overstates the degree of end-to-end mechanical certification actually achieved for the suite of open problems.
minor comments (5)
  1. [Abstract; §5] Abstract and §1 state that 11 problems were solved; the Conclusion (§5) says “ten problems.” Align the count with Table 4.
  2. [Figure 2; §2.3] Figure 1 and Figure 2 captions and body text refer to “orange regions” for the Augmentation Plane while the surrounding prose describes it as green; colour consistency would aid readability.
  3. [References] Several companion results are cited as 2026 arXiv preprints without DOIs or stable identifiers beyond arXiv numbers; adding version pins or permanent links would improve reproducibility.
  4. [§3; §4] The manuscript never names the concrete base LLMs (or coding agents such as Claude Code / Codex) used inside the Orchestrator and subagents, nor the compute budget of the two-month deployment; a short implementation appendix would help replication.
  5. [Table 1a; §4.1–4.3] Table 1a lists twelve specialist roles; a brief mapping of which roles were actually invoked in each of the three case studies would make the agent traces easier to follow.

Circularity Check

2 steps flagged

The '11 problems solved' co-pilot claim is load-bearing on same-team companion arXiv papers whose human vs. MMAT contribution share is unquantified, so evaluation reduces to self-citation of joint outputs.

specific steps
  1. self citation load bearing [Abstract; §1; Table 4; §4 intro; refs. [6–8,14,15,19,20,36,51]]
    "Across a two-month deployment, 11 problems have been solved, demonstrating its capacity to act as a co-pilot throughout the entire research cycle. ... Over a two-month internal experience period by authors and collaborators, MMAT solved 11 mathematical problems (Table 4 and Figure 8) ... Among these advancements, MMAT either provides a rigorous proof of the key theorem or fully automates the derivation of the complete result. ... The “Human” column indicates whether the work involved human participation ... To date, we have uploaded nine completed works to arXiv."

    The load-bearing empirical premise (MMAT solved 11 open problems as co-pilot) is justified only by companion arXiv papers whose author lists overlap with the present paper. Table 4 marks Human ✓ for most entries and Formal only for a subset, yet the manuscript never quantifies human strategic inputs, breakpoints (§2.3.1), or lemma/route ownership versus agents. The evaluation therefore cites the joint human–AI outputs being evaluated; no external benchmark or independent replication breaks the loop. Lean formalization (where present) checks the math, not MMAT’s causal contribution.

  2. self citation load bearing [§4.3; Figure 8; refs. [8,19,20,36]]
    "Sparse polynomial computation serves as a running case study in this section. ... Settle the problem over integers [20]. ... Sparse polynomial divisibility test over finite fields CoNP-hard [8]. ... Output-sensitive GCD over finite field is NP-hard [36]. ... Multi-variate case of the conjecture ... [19]."

    Project-level success (six sparse-polynomial problems resolved) is again evidenced by same-team companion papers. The audit of Giorgi et al. and the subsequent reconstruction are presented as MMAT-driven, but the published resolutions are co-authored by the MMAT team and the Human column remains ✓; the manuscript does not isolate which steps were agent-only versus human-directed, so the project-level co-pilot claim again rests on self-citation of the outputs under evaluation.

full rationale

This is a systems/architecture paper, not a first-principles derivation paper; the Harness design, agent roles, and case-study pipelines are self-contained engineering descriptions and are not circular by construction. The circularity is confined to the central empirical claim that MMAT solved 11 open problems as co-pilot across the full research cycle. That claim is evidenced almost exclusively by companion arXiv preprints co-authored by the same team (Table 4; refs. [6–8,14,15,19,20,36,51] etc.), with the Human column marking participation for most entries but supplying no counts of intervention breakpoints, strategic inputs, or fraction of novel lemmas/routes from humans versus agents. Formal Lean checks (where present) certify mathematical correctness of the companion results, not that MMAT autonomously produced them or that the Harness was necessary. There is no external benchmark suite, third-party replication, or ablation that separates system contribution from human-led research assisted by LLM tools. This is partial (evaluation-loop) circularity via self-citation, not definitional circularity in the math itself; architecture content remains independent. Score 6 reflects that the headline empirical claim reduces to the self-citation chain, while the rest of the paper does not.

Axiom & Free-Parameter Ledger

0 free parameters · 4 axioms · 2 invented entities

The paper’s claims rest on standard correctness of Lean 4, on the engineering assumptions of the Harness planes, and on the status of the 11 problems as previously open. No numerical free parameters are fitted; the invented entities are the architecture and agent suite themselves.

axioms (4)
  • standard math Lean 4 kernel correctly decides mathematical validity of the formalized statements
    FL-Prover treats the compiler as the sole ground-truth oracle (§3.2).
  • domain assumption Isolated workspaces plus file-based hand-offs contain reasoning errors and prevent context bloat
    Core design claim of the Execution Plane (§2.2).
  • domain assumption The 11 problems listed in Table 4 were open prior to the two-month MMAT deployment
    Required for the empirical success claim (Abstract, §4).
  • ad hoc to paper Human-in-the-loop breakpoints do not reduce the system to a pure human-driven workflow
    Augmentation Plane (§2.3) and Human column of Table 4; the paper asserts co-pilot status despite frequent human marks.
invented entities (2)
  • Harness Architecture (Control / Execution / Augmentation planes) no independent evidence
    purpose: Decouple scheduling, isolation and cognitive scaffolding for long-horizon multi-agent math research
    Introduced as the primary architectural contribution in §2; no prior identical three-plane design is cited.
  • MMAT closed-loop agents (KB-Manager, NL-Prover, FL-Prover) no independent evidence
    purpose: Produce formally certified proofs via Inform–Formalize–Feedback–Archive cycle
    Instantiated in §3; the typed card schema and specialist sub-agent swarm are new constructs.

pith-pipeline@v1.1.0-grok45 · 28386 in / 2742 out tokens · 47064 ms · 2026-07-11T19:28:47.760274+00:00 · methodology

0 comments
read the original abstract

AI reasoning has become a central focus in contemporary artificial intelligence, largely driven by the success of large language models. However, mathematical research, which is characterized by non-linear derivation paths, rigorous logical requirements, and protracted exploration cycles, poses severe challenges for existing reasoning systems. To overcome these limitations, we present the MechMath Agent Team (MMAT), which is a large language model driven agent designed to serve as a co-pilot throughout the full cycle of mathematical research. We design a tripartite Harness Architecture that decouples system responsibilities into Control, Execution, and Augmentation planes, thereby reconciling rigorous logical control with the agility demanded by open-ended research. Building upon this framework, we instantiate three specialized agents: a Knowledge Base Manager, a Natural Language Prover, and a Formal Language Prover, all operating in a closed loop to produce formally certified mathematical proofs. We evaluate MMAT on open problems in Number Theory, Algebraic Complexity Theory, Differential Algebra, Operator Algebra, and Inequalities. Across a two-month deployment, 11 problems have been solved, demonstrating its capacity to act as a co-pilot throughout the entire research cycle. The contributions are threefold: a general decoupled Harness Architecture for multi-agent mathematical reasoning, its concrete instantiation in the MMAT system, and empirical validation on a diverse suite of open problems.

Figures

Figures reproduced from arXiv: 2607.04394 by Dakai Guo, Jiaqi Wang, Junqi Liu, Lihong Zhi, Ruichen Qiu, Ruyong Feng, Xiao-Shan Gao, Yichuan Cao.

Figure 1
Figure 1. Figure 1: Architectural of the MechMath Agent Team. The underlying [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The Harness Architecture. The whole architecture can be divided into three parts: The control plane (blue [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: System architecture and collaborative workflow of the MechMath Agent Team. Center of the diagram shows [PITH_FULL_IMAGE:figures/full_fig_p008_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Knowledge Base for Sparse Polynomials. We highlight all related cards to the concept of “Factor Sparsity [PITH_FULL_IMAGE:figures/full_fig_p013_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: The multi-agent theorem proving pipeline example of [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Orchestrated flow in proving Vasc’s Cyclic Inequality for [PITH_FULL_IMAGE:figures/full_fig_p018_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The agent-driven verification and counterexample discovery framework. (a) [PITH_FULL_IMAGE:figures/full_fig_p020_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Project on Sparse polynomial with MMAT. Through interaction with [PITH_FULL_IMAGE:figures/full_fig_p020_8.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

53 extracted references · 16 linked inside Pith

  1. [1]

    QED: An open-source multi-agent sys- tem for generating mathematical proofs on open problems

    Chenyang An, Qihao Ye, Minghao Pan, and Jiayun Zhang. QED: An open-source multi-agent sys- tem for generating mathematical proofs on open problems. In3rd AI for Math Workshop: Toward Self- Evolving Scientific Agents, 2026

    2026

  2. [2]

    Leanexplore: A search engine for lean 4 declarations, 2025

    Justin Asher. Leanexplore: A search engine for lean 4 declarations, 2025. URLhttps://arxiv.org/ abs/2506.11085

    Pith/arXiv arXiv 2025

  3. [3]

    Traceability and accountability in role-specialized multi-agent llm pipelines

    Amine Barrak. Traceability and accountability in role-specialized multi-agent llm pipelines. In2025 40th IEEE/ACM International Conference on Automated Software Engineering Workshops (ASEW), pp. 315– 322, 2025

    2025

  4. [4]

    Deterministic factorization of sparse polyno- mials with bounded individual degree.Journal of the ACM, 67(2):Article 8, 2020

    Vishwas Bhargava, Shubhangi Saraf, and Ilya Volkovich. Deterministic factorization of sparse polyno- mials with bounded individual degree.Journal of the ACM, 67(2):Article 8, 2020

    2020

  5. [5]

    Maurice Rojas

    Jingguo Bi, Qi Cheng, and J. Maurice Rojas. Sublinear root detection and new hardness results for sparse polynomials over finite fields.SIAM Journal on Computing, 45(4):1433–1447, 2016

    2016

  6. [6]

    The equivalence problem for generalized airy operators, 2026

    Yichuan Cao, Ruyong Feng, Yunfei Li, and Ruichen Qiu. The equivalence problem for generalized airy operators, 2026. URLhttps://arxiv.org/abs/2607.00359

    Pith/arXiv arXiv 2026

  7. [7]

    Every nonnegative integer is a sum of a triangular, a pentagonal, and a heptagonal number, 2026

    Yichuan Cao, Dakai Guo, Ruichen Qiu, Ruyong Feng, and Xiao-Shan Gao. Every nonnegative integer is a sum of a triangular, a pentagonal, and a heptagonal number, 2026. URLhttps://arxiv.org/abs/ 2606.26035

    Pith/arXiv arXiv 2026

  8. [8]

    Sparse polynomial divisibility test over finite field is conp-hard, 2026

    Yichuan Cao, Ruichen Qiu, Qiao-Long Huang, Ruyong Feng, and Xiao-Shan Gao. Sparse polynomial divisibility test over finite field is conp-hard, 2026. 21 Key Laboratory of Mathematics Mechanization MechMath Agent Team

    2026

  9. [9]

    Cohesive conversations: Enhancing authenticity in multi-agent simulated dialogues

    KuanChao Chu, Yi-Pei Chen, and Hideki Nakayama. Cohesive conversations: Enhancing authenticity in multi-agent simulated dialogues. InFirst Conference on Language Modeling, 2024

    2024

  10. [10]

    The sparsity challenges

    James Harold Davenport and Jacques Carette. The sparsity challenges. InProc. 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC’09, pp. 3–7, 2009

    2009

  11. [11]

    P . Erdös. On the number of terms of the square of a polynomial.Nieuw Arch. Wiskd., 23(2):63–65, 1949

    1949

  12. [12]

    Leansearch v2: Global premise retrieval for lean 4 theorem proving, 2026

    Guoxiong Gao, Zeming Sun, Jiedong Jiang, Yutong Wang, Jingda Xu, Peihao Wu, Bryan Dai, and Bin Dong. Leansearch v2: Global premise retrieval for lean 4 theorem proving, 2026. URLhttps: //arxiv.org/abs/2605.13137

    Pith/arXiv arXiv 2026

  13. [13]

    Essentially optimal sparse polynomial mul- tiplication

    Pascal Giorgi, Bruno Grenet, and Armelle Perret du Cray. Essentially optimal sparse polynomial mul- tiplication. InProceedings of the 45th International Symposium on Symbolic and Algebraic Computation, ISSAC ’20, pp. 202–209, New York, NY, USA, 2020. Association for Computing Machinery

    2020

  14. [14]

    A finite certificate for the positiven=9 vasc inequality, 2026

    Dakai Guo, Ruichen Qiu, Yichuan Cao, and Ruyong Feng. A finite certificate for the positiven=9 vasc inequality, 2026. URLhttps://arxiv.org/abs/2606.06136

    Pith/arXiv arXiv 2026

  15. [15]

    A greatest common divisor criterion of certain binomial coefficients, 2026

    Dakai Guo, Ruichen Qiu, Yichuan Cao, Ruyong Feng, and Xiao-Shan Gao. A greatest common divisor criterion of certain binomial coefficients, 2026. URLhttps://arxiv.org/abs/2606.22997

    Pith/arXiv arXiv 2026

  16. [16]

    Metagpt: Meta programming for a multi-agent collaborative framework

    Sirui Hong, Mingchen Zhuge, Jonathan Chen, Xiawu Zheng, Yuheng Cheng, Jinlin Wang, Ceyao Zhang, zili wang, Steven Yau, Zijuan Lin, Liyang Zhou, Chenyu Ran, Lingfeng Xiao, Chenglin Wu, and Jürgen Schmidhuber. Metagpt: Meta programming for a multi-agent collaborative framework. In B. Kim, Y. Yue, S. Chaudhuri, K. Fragkiadaki, M. Khan, and Y. Sun (eds.),Inte...

    2024

  17. [17]

    Large language models cannot self-correct reasoning yet

    Jie Huang, Xinyun Chen, Swaroop Mishra, Huaixiu Steven Zheng, Adams Yu, Xinying Song, and Denny Zhou. Large language models cannot self-correct reasoning yet. In B. Kim, Y. Yue, S. Chaudhuri, K. Fragkiadaki, M. Khan, and Y. Sun (eds.),International Conference on Learning Representations, volume 2024, pp. 32808–32824, 2024

    2024

  18. [18]

    Sparse polynomial interpolation over fields with large or zero characteristic

    Qiao-Long Huang. Sparse polynomial interpolation over fields with large or zero characteristic. In Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation, ISSAC ’19, pp. 219–226, New York, NY, USA, 2019. Association for Computing Machinery

    2019

  19. [19]

    Deterministic polynomial-time exact-root computation for sparse polynomials with bounded total degree, 2026

    Qiao-Long Huang, Yichuan Cao, Ruichen Qiu, and Xiao-Shan Gao. Deterministic polynomial-time exact-root computation for sparse polynomials with bounded total degree, 2026. URLhttps://arxiv. org/abs/2607.02364

    Pith/arXiv arXiv 2026

  20. [20]

    Quasi-linear time multiplication of sparse polynomials with integer coefficients, 2026

    Qiao-Long Huang, Yichuan Cao, Ruichen Qiu, and Xiao-Shan Gao. Quasi-linear time multiplication of sparse polynomials with integer coefficients, 2026. URLhttps://arxiv.org/abs/2606.12100

    Pith/arXiv arXiv 2026

  21. [21]

    Understanding the planning of llm agents: A survey, 2024

    Xu Huang, Weiwen Liu, Xiaolong Chen, Xingmei Wang, Hao Wang, Defu Lian, Yasheng Wang, Ruim- ing Tang, and Enhong Chen. Understanding the planning of llm agents: A survey, 2024. URL https://arxiv.org/abs/2402.02716

    Pith/arXiv arXiv 2024

  22. [22]

    Yichen Huang and Lin F. Yang. Winning gold at imo 2025 with a model-agnostic verification-and- refinement pipeline, 2025. URLhttps://arxiv.org/abs/2507.15855

    arXiv 2025

  23. [23]

    Survey of hallucination in natural language generation.ACM Comput

    Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Ye Jin Bang, Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation.ACM Comput. Surv., 55(12), March 2023. ISSN 0360-0300

    2023

  24. [24]

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

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. InThe Eleventh International Conference on Learning Representations, 2023

    2023

  25. [25]

    Matlas: A semantic search engine for mathematics, 2026

    Haocheng Ju, Leheng Chen, Peihao Wu, Bryan Dai, and Bin Dong. Matlas: A semantic search engine for mathematics, 2026. URLhttps://arxiv.org/abs/2604.17484

    Pith/arXiv arXiv 2026

  26. [26]

    LLM Wiki

    Andrej Karpathy. LLM Wiki. Technical report, 2026. URLhttps://gist.github.com/karpathy/ 442a6bf555914893e9891c11519de94f. 22 Key Laboratory of Mathematics Mechanization MechMath Agent Team

    2026

  27. [27]

    On the calculation of some differential galois groups.Inventiones mathematicae, 87(1): 13–61, 1987

    Nicholas M Katz. On the calculation of some differential galois groups.Inventiones mathematicae, 87(1): 13–61, 1987

    1987

  28. [28]

    Numina-lean-agent: An open and general agentic reasoning system for formal mathematics, 2026

    Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, and Wenda Li. Numina-lean-agent: An open and general agentic reasoning system for formal mathematics, 2026. URLhttps://arxiv.org/abs/ 2601.14027

    arXiv 2026

  29. [29]

    Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang

    Nelson F. Liu, Kevin Lin, John Hewitt, Ashwin Paranjape, Michele Bevilacqua, Fabio Petroni, and Percy Liang. Lost in the middle: How language models use long contexts.Transactions of the Association for Computational Linguistics, 12:157–173, 2024

    2024

  30. [30]

    Lean finder: Semantic search for mathlib that understands user intents, 2026

    Jialin Lu, Kye Emond, Kaiyu Yang, Swarat Chaudhuri, Weiran Sun, and Wuyang Chen. Lean finder: Semantic search for mathlib that understands user intents, 2026. URLhttps://arxiv.org/abs/2510. 15940

    2026

  31. [31]

    A proposal for the dartmouth summer research project on artificial intelligence, august 31, 1955.AI magazine, 27(4):12–12, 2006

    John McCarthy, Marvin L Minsky, Nathaniel Rochester, and Claude E Shannon. A proposal for the dartmouth summer research project on artificial intelligence, august 31, 1955.AI magazine, 27(4):12–12, 2006

    1955

  32. [32]

    Patil, Ion Stoica, and Joseph E

    Charles Packer, Sarah Wooders, Kevin Lin, Vivian Fang, Shishir G. Patil, Ion Stoica, and Joseph E. Gonzalez. Memgpt: Towards llms as operating systems, 2024. URLhttps://arxiv.org/abs/2310. 08560

    2024

  33. [33]

    Knowledge graph refinement: A survey of approaches and evaluation methods

    Heiko Paulheim. Knowledge graph refinement: A survey of approaches and evaluation methods. Semantic web, 8(3):489–508, 2016

    2016

  34. [34]

    New np-hard and np-complete polynomial and integer divisibility problems

    David Alan Plaisted. New np-hard and np-complete polynomial and integer divisibility problems. Theoretical Computer Science, 31(1):125–138, 1984

    1984

  35. [35]

    Beyond individual intelligence: Surveying collaboration, failure attribution, and self-evolution in llm-based multi-agent systems, 2026

    Shihao Qi, Jie Ma, Rui Xing, Wei Guo, Xiao Huang, Zhitao Gao, Jianhao Deng, Jun Liu, Lingling Zhang, Bifan Wei, Boqian Yang, Pinghui Wang, Jianwen Sun, Jing Tao, Yaqiang Wu, Hui Liu, Yu Yao, and Tongliang Liu. Beyond individual intelligence: Surveying collaboration, failure attribution, and self-evolution in llm-based multi-agent systems, 2026. URLhttps:/...

    Pith/arXiv arXiv 2026

  36. [36]

    Output-sensitive sparse polynomial gcd over finite fields is np-hard, 2026

    Ruichen Qiu, Yichuan Cao, Qiao-Long Huang, Ruyong Feng, and Xiao-Shan Gao. Output-sensitive sparse polynomial gcd over finite fields is np-hard, 2026. URLhttps://arxiv.org/abs/2606.12144

    Pith/arXiv arXiv 2026

  37. [37]

    Code generation with alphacodium: From prompt engineering to flow engineering, 2024

    Tal Ridnik, Dedy Kredo, and Itamar Friedman. Code generation with alphacodium: From prompt engineering to flow engineering, 2024. URLhttps://arxiv.org/abs/2401.08500

    Pith/arXiv arXiv 2024

  38. [38]

    Daniel S. Roche. What can (and can’t) we do with sparse polynomials? InProc. ISSAC, ISSAC’18, pp. 16–19, 2018

    2018

  39. [39]

    Daniel S. Roche. What can (and can’t) we do with sparse polynomials? InProceedings of the 2018 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC ’18, pp. 25–30, New York, NY, USA, 2018. Association for Computing Machinery

    2018

  40. [40]

    Aaai 2025 presidential panel on the future of ai research.Association for the Advancement of Artificial Intelli- gence, Washington, DC, 2025

    Francesca Rossi, Christian Bessiere, Joydeep Biswas, R Brooks, V Conitzer, TG Dietterich, et al. Aaai 2025 presidential panel on the future of ai research.Association for the Advancement of Artificial Intelli- gence, Washington, DC, 2025

    2025

  41. [41]

    Schinzel

    A. Schinzel. On the number of terms of a power of a polynomial.Acta Arithmetica, XLIX:55–70, 1997

    1997

  42. [42]

    prove a cyclic inequality

    Sil. Answer to “prove a cyclic inequality” (xia–yang references). Mathematics Stack Exchange, 2023. URLhttps://math.stackexchange.com/a/4693459

    arXiv 2023

  43. [43]

    Brown, Adam Santoro, and et al

    Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, and et al. Beyond the imitation game: Quantifying and ex- trapolating the capabilities of language models.Transactions on Machine Learning Research, 2023. ISSN 2835-8856. Featured Certification. 23 Key Laboratory of Mathematics Mech...

    2023

  44. [44]

    Mistake notebook learning: Batch-clustered failures for training-free agent adaptation

    Xuanbo Su, Yingfang Zhang, Hao Luo, Xiaoteng Liu, and Leo Huang. Mistake notebook learning: Batch-clustered failures for training-free agent adaptation. In Maria Liakata, Viviane P . Moreira, Jiajun Zhang, and David Jurgens (eds.),Findings of the Association for Computational Linguistics: ACL 2026, pp. 14629–14645, San Diego, California, United States, Ju...

    2026

  45. [45]

    A makespan and energy-aware scheduling algorithm for workflows under reliability constraint on a multiprocessor platform, 2022

    Atharva Tekawade and Suman Banerjee. A makespan and energy-aware scheduling algorithm for workflows under reliability constraint on a multiprocessor platform, 2022. URLhttps://arxiv.org/ abs/2212.09274

    Pith/arXiv arXiv 2022

  46. [46]

    Factoring sparse multivariate polynomials.Journal of Computer and System Sciences, 31(2):265–287, 1985

    Joachim von zur Gathen and Erich Kaltofen. Factoring sparse multivariate polynomials.Journal of Computer and System Sciences, 31(2):265–287, 1985

    1985

  47. [47]

    A survey on large language model based autonomous agents.Frontiers of Computer Science, 18(6):186345, 2024

    Lei Wang, Chen Ma, Xueyang Feng, Zeyu Zhang, Hao Yang, Jingsen Zhang, Zhiyuan Chen, Jiakai Tang, Xu Chen, Yankai Lin, Wayne Xin Zhao, Zhewei Wei, and Jirong Wen. A survey on large language model based autonomous agents.Frontiers of Computer Science, 18(6):186345, 2024. ISSN 2095-2236

    2024

  48. [48]

    Chain-of-thought prompting elicits reasoning in large language models

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou. Chain-of-thought prompting elicits reasoning in large language models. In S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh (eds.),Advances in Neural Infor- mation Processing Systems, volume 35, pp. 24824–24837. Curran Associat...

    2022

  49. [49]

    World Scientific, 2016

    Bican Xia and Lu Yang.Automated Inequality Proving and Discovering. World Scientific, 2016

    2016

  50. [50]

    From spark to fire: Modeling and mitigating error cascades in llm-based multi-agent collaboration, 2026

    Yizhe Xie, Congcong Zhu, Xinyue Zhang, Tianqing Zhu, Dayong Ye, Minfeng Qi, Huajie Chen, and Wanlei Zhou. From spark to fire: Modeling and mitigating error cascades in llm-based multi-agent collaboration, 2026. URLhttps://arxiv.org/abs/2603.04474

    Pith/arXiv arXiv 2026

  51. [51]

    Complexity of low-degree skew polynomial multiplication over finite fields, 2026

    Ke Ye, Yichuan Cao, and Ruichen Qiu. Complexity of low-degree skew polynomial multiplication over finite fields, 2026. URLhttps://arxiv.org/abs/2607.00476

    Pith/arXiv arXiv 2026

  52. [52]

    J. Yu, Y. Ding, and H. Sato. Dyntaskmas: A dynamic task graph-driven framework for asynchronous and parallel llm-based multi-agent systems.Proceedings of the International Conference on Automated Planning and Scheduling, 35(1):288–296, 2025

    2025

  53. [53]

    On composite lacunary polynomials and the proof of a conjecture of Schinzel.In- ventiones Mathematicae, 174:127–138, 2008

    Umberto Zannier. On composite lacunary polynomials and the proof of a conjecture of Schinzel.In- ventiones Mathematicae, 174:127–138, 2008. 24

    2008