PACE: Research Proving Agent for Adaptive Conjecture Exploration

Shu Miao; Feiming Wang; Wentao Long; Chenyi Li; Kun Yuan; Zaiwen Wen

cs.AIOct 24, 2026

PACE: Research Proving Agent for Adaptive Conjecture Exploration

Authors: Shu Miao, Feiming Wang, Wentao Long, Chenyi Li, Kun Yuan, Zaiwen Wen

Organizations: Peking University · Nankai University · Fudan University

Abstract

Many mathematical research agents focus on solving problems with fixed statements. However, conjecture research, especially in applied mathematics, may require revising candidate questions or conclusions as investigation proceeds, coupling problem formulation with proof development. We present PACE, a research-proof agent that supports this process through a structured research loop that selects mathematical objectives and develops or challenges candidate mechanisms. The whole prover constructs proofs from these mechanisms, and an independent verifier checks them against the original target. Evidence-tracking memory stores assumptions and dependencies arising during research and marks evidence for revalidation when a candidate or condition changes. This memory supports task-specific context composition that keeps checked premises, exploratory material and unresolved obligations distinct. To evaluate proof construction and conjecture research, we introduce ResearchProofBench, an applied-mathematics benchmark focused on optimization, comprising 51 known-proof tasks with 331 hidden checkpoints under historical abstract access and six open-problem cases. The known-proof tasks assess reconstruction of published results, while the open-problem cases assess mathematical investigation and proof development. On the 51 known-proof tasks, PACE achieves an aggregate Proof Score of 75.16 and completes 20 proofs. In conjecture research, PACE develops conditional results, with its submissions receiving higher review scores than the compared baselines.

Figures & tables

System	Plan subproblems	Refine conjectures	Record result conditions	Recheck support after revisions	Separate prompt composition
QED	$\checkmark$	—	$\checkmark$	—	—
Iteris	$\checkmark$	$\checkmark$	$\checkmark$	—	—
PACE	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$

Table 1: Research mechanisms in QED ( An et al., 2026 ) , Iteris ( Chen et al., 2026 ) and PACE.

Figure 1: Overview of PACE for direct proving and conjecture research.

Figure 2: Candidate and mechanism refinement in RCI.

Input: original target $T_{0}$ , initial memory $M_{0}$ , investigation limit $\tau$ .
	Frame $T_{0}$ into subproblems $W_{0}$ and initialize $s_{0}$ with $M_{0}$ .
	for $t=0,\ldots,\tau-1$ do
	Select objective $g_{t}$ and action $a_{t}$ from $s_{t}$ ; execute $a_{t}$ using $\operatorname{Ctx}_{t}(g_{t})$ to obtain $z_{t}$ .
	If $z_{t}$ is a complete candidate proof, have the auditor and mathematical reviewer assess it against $T_{0}$ and record their findings.
	Identify $\mathcal{D}_{t}$ , $\mathcal{N}_{t}$ and $\mathcal{B}_{t}$ from the result, current support assessments and any review findings.
	$\mathcal{O}_{t+1}\leftarrow(\mathcal{O}_{t}\setminus\mathcal{D}_{t})\cup\mathcal{N}_{t}\cup\mathcal{B}_{t}$ .

Algorithm 1 Research program and proof development

System	Proof Score	Weighted Obligation Completion (%)	CPR (%)
direct prompting	59.25	41.02	21.57
self-check prompting	60.87	44.08	27.45
QED	62.22	41.49	17.65
Rethlas	67.33	49.37	31.37
Iteris	68.05	50.78	33.33
PACE	75.16	60.75	39.22

Table 2: Known-proof results on 51 tasks per method: component-level scores and theorem-level completion.

ID	Submission	LLM	Human	Conclusion	Main gap or qualification
C1	Direct Solving	2	2	Conditional smoothness reduction	Invalid refutations
	Iterative Solving	3	3	Conditional upper-bound progress	Initial objective gap omitted
	PACE	7	6	Task-permitted conditional result	Local exposition gap
C2	Direct Solving	2	1	Sample normalization	Minimax proof absent
	Iterative Solving	2	2	Source normalization	Minimax resolution absent
	PACE	5	5	Fixed-path span lower bound	Source certification missing

Table 3: Conjecture-research outcomes with LLM and human scores on the 0–7 scale.

Variant	LLM score	Human score
Full system	7	6
Single-Pass Research–Proof	3	3
Fixed-prompt workflow	6	5
Predetermined research sequence	6	4
Proof critique and revision	5	3
Without the revision-triggered revalidation module	3	2

Table 4: Five research workflow ablations on C1, with the full system as reference.

Access	Proof Score	Weighted Obligation Completion (%)	Complete Proof Rate (%)
No-web	70.28	54.55	35.29
Frozen clean-web	75.16	60.75	39.22
Live full-web	80.82	68.90	56.86

Table 5: Full-system search ablations with architecture fixed.

Appendix figures & tables18 assets

Supplementary material from the paper’s appendix.

Appendix

Cluster	Tasks	Main mathematical content
P01	1	Recurrence comparison and nonasymptotic bounds
P02	2	Regularized quasi-Newton complexity
P04	3	Interpolation, stepsize sequences and sharpness
P06	2	Exact-penalty subproblems and duality
P08	2	Local subgradient geometry and smoothing
P10	4	Primal–dual fixed points, identification and restart

Appendix

Table 6: Source-paper clusters in the known-proof component.

Task	Source result	Difficulty	Checkpoints
P01-T01	Theorem 1	S2	6
P02-T02	Lemma 19	S1	7
P02-T03	Theorem 22	S2	7
P04-T04	Proposition 2.17	S2	6
P04-T05	Lemma 4.3	S2	6
P04-T06	Lemma 5.4	S2	6

Appendix

Table 7: Known-Proof task inventory (1/2).

Task	Source result	Difficulty	Checkpoints
P16-T01	Proposition 7.1	S2	6
P16-T02	Theorem 7.3	S2	6
P17-T01	Theorem 3	S2	6
P17-T02	Theorem 4	S2	7
P17-T03	Lemma 3	S1	6
P18-T01	Theorem 4	S3	6

Appendix

Table 8: Known-Proof task inventory (2/2).

Grade	Required mathematical evidence
4	A complete, correct derivation, including hypotheses, quantifiers, constants, signs, branches and theorem applicability; the reviewer need not supply a missing argument.
3	The derivation is correct apart from a minor local rigor gap.
2	Valid progress is present, but a necessary bridge remains unproved.
1	A relevant proof attempt contains a mathematical error or invalid argument.
0	No supporting derivation of the registered claim is supplied.

Appendix

Table 9: Atomic grades for registered mathematical claims.

System	Reviewed tasks	Complete obligations	Weighted Obligation Completion (%)
direct prompting	51/51	146/331	41.02
self-check prompting	51/51	155/331	44.08
QED	51/51	152/331	41.49
Rethlas	51/51	171/331	49.37
Iteris	51/51	178/331	50.78
PACE	51/51	206/331	60.75

Appendix

Table 10: Final weighted obligation completion for the same records as Table 2 . Obligation counts are descriptive; Weighted Obligation Completion uses task-specific weights and equal averaging over 51 tasks.

Available	Literal task, permitted assumptions, anonymized final proof and referenced proof bodies, hidden reference, registered claims, weights and dependencies
Excluded	System identity, internal acceptance labels, other submissions and other review judgments
Model output	Atomic grades, route classifications, mathematical explanations, gap records and supporting, contextual, or contradicting line references
Derived output	Effective grades, checkpoint points, additional deductions, Proof Score and weighted obligation completion
CPR decision	Target conclusion, admissible assumptions and a justified proof route, assessed from the mathematical explanations and gap records

Appendix

Table 11: Inputs and outputs of one independent mathematical review.

Task	Direct Prompting	Self-Check Prompting	QED	Rethlas	Iteris
P01-T01	$58.67\,/\,38.00$	$51.67\,/\,12.00$	$100.00\,/\,100.00$	$100.00\,/\,100.00$	$100.00\,/\,100.00$
P02-T02	$70.67\,/\,48.00$	$64.33\,/\,24.00$	$53.00\,/\,24.00$	$53.00\,/\,24.00$	$100.00\,/\,100.00$
P02-T03	$96.67\,/\,90.00$	$100.00\,/\,100.00$	$39.50\,/\,0.00$	$46.50\,/\,0.00$	$50.00\,/\,0.00$
P04-T04	$36.00\,/\,12.00$	$44.33\,/\,12.00$	$28.33\,/\,0.00$	$100.00\,/\,100.00$	$69.00\,/\,38.00$
P04-T05	$39.33\,/\,22.00$	$45.33\,/\,22.00$	$29.83\,/\,0.00$	$47.67\,/\,10.00$	$47.67\,/\,10.00$
P04-T06	$0.00\,/\,0.00$	$0.00\,/\,0.00$	$51.00\,/\,10.00$	$51.00\,/\,10.00$	$51.00\,/\,10.00$

Appendix

Table 12: Final Known-Proof results (1/2). Each entry is Proof Score / Weighted Obligation Completion (%), computed from the same accepted review.

Task	Direct Prompting	Self-Check Prompting	QED	Rethlas	Iteris
P17-T01	$65.33\,/\,60.00$	$65.33\,/\,60.00$	$45.83\,/\,18.00$	$100.00\,/\,100.00$	$65.33\,/\,60.00$
P17-T02	$92.33\,/\,74.00$	$82.33\,/\,68.00$	$56.83\,/\,24.00$	$56.00\,/\,24.00$	$71.67\,/\,46.00$
P17-T03	$100.00\,/\,100.00$	$100.00\,/\,100.00$	$59.67\,/\,18.00$	$86.83\,/\,42.00$	$86.83\,/\,42.00$
P18-T01	$19.00\,/\,12.00$	$19.00\,/\,12.00$	$27.17\,/\,12.00$	$23.67\,/\,12.00$	$25.17\,/\,12.00$
P18-T02	$100.00\,/\,100.00$	$100.00\,/\,100.00$	$100.00\,/\,100.00$	$100.00\,/\,100.00$	$100.00\,/\,100.00$
P19-T01	$35.00\,/\,12.00$	$14.33\,/\,0.00$	$58.00\,/\,58.00$	$60.67\,/\,58.00$	$58.00\,/\,58.00$

Appendix

Table 13: Final Known-Proof results (2/2). Each entry is Proof Score / Weighted Obligation Completion (%), computed from the same accepted review.

Task	Proof Score	Weighted Obligation Completion (%)	Task	Proof Score	Weighted Obligation Completion (%)
P01-T01	100.00	100.00	P17-T01	69.33	60.00
P02-T02	100.00	100.00	P17-T02	89.00	64.00
P02-T03	98.33	90.00	P17-T03	81.00	58.00
P04-T04	69.00	38.00	P18-T01	30.33	12.00
P04-T05	100.00	100.00	P18-T02	100.00	100.00
P04-T06	6.00	0.00	P19-T01	56.00	46.00

Appendix

Table 14: Final PACE results on all 51 Known-Proof tasks. The two panels list disjoint task subsets. Each row reports Proof Score and Weighted Obligation Completion (%); a score of 100 identifies full completion of the registered obligations with no remaining gap.

System	$n$	Proof Score	Weighted Obligation Completion (%)	Complete Proof Rate (%)
Direct Prompting	11	66.70	55.09	4/11 (36.36)
Self-Check Prompting	11	69.47	56.55	4/11 (36.36)
QED	11	67.09	47.27	3/11 (27.27)
Rethlas	11	67.29	49.09	3/11 (27.27)
Iteris	11	79.08	68.36	6/11 (54.55)
PACE	11	81.33	72.18	6/11 (54.55)

Appendix

Table 15: Known-Proof results for S1 tasks (11 tasks).

System	$n$	Proof Score	Weighted Obligation Completion (%)	Complete Proof Rate (%)
Direct Prompting	29	55.60	34.83	4/29 (13.79)
Self-Check Prompting	29	57.34	37.86	6/29 (20.69)
QED	29	56.38	32.55	2/29 (6.90)
Rethlas	29	64.15	44.55	9/29 (31.03)
Iteris	29	61.62	40.48	7/29 (24.14)
PACE	29	72.89	55.79	9/29 (31.03)

Appendix

Table 16: Known-Proof results for S2 tasks (29 tasks).

System	$n$	Proof Score	Weighted Obligation Completion (%)	Complete Proof Rate (%)
Direct Prompting	11	61.44	43.27	3/11 (27.27)
Self-Check Prompting	11	61.54	48.00	4/11 (36.36)
QED	11	72.74	59.27	4/11 (36.36)
Rethlas	11	75.76	62.36	4/11 (36.36)
Iteris	11	73.97	60.36	4/11 (36.36)
PACE	11	75.00	62.36	5/11 (45.45)

Appendix

Table 17: Known-Proof results for S3 tasks (11 tasks).

Aspect	YUAN [1984]	C6 construction
Regularity	Convex $C^{2}$ objective; positive-definite Hessian at the minimizer	Globally $C^{\infty}$ and strongly convex example in the task’s locally strongly convex class
Q-order	Adjacent-iterate Q-orders $1+1/N$ for arbitrarily large $N$	Adjacent-iterate Q-order exactly one under Eq. ( 6 )
Attainment	Infimum one obtained from a family of runs	One infinite run attains the infimum in each fixed dimension
Algorithm	Broyden-family updates, including BFGS, with perfect line searches	Hessian-form BFGS with global minimization on every search line
Dimension	Every fixed $n\geq 2$ , by extension of the two-dimensional example	Every fixed $n\geq 2$ , preserving BFGS and Q-order under a block lift

Appendix

Table 18: C6 compared with the classical least-Q-order result.

Object	Host checks or records	Model judgment
Dispatch	Roles, limits, input references	Objective and action selection
Revision	Content change, version, review reset	Mathematical meaning of change
Reuse	Sources and historical arguments	Applicability and valid inference
Review	Same target and current candidate	Scope and argument correctness

Appendix

Table 19: Operational checks and semantic decisions.

Component	Main responsibility	Output and authority
director	Select one next action and its inputs	Scheduling directive; no mathematical verdict
prompt composer	Organize a selected task and its mathematical inputs	Role-specific prompt; no scheduling decision or mathematical verdict
survey	Acquire and inspect permitted sources	Source records and applicability gaps
research framing	Organize the original request	Bounded work items and dependencies
RCI	Develop candidates and support	Candidate tasks, mechanisms, uncovered regions and refutations
planner	Develop or substantially revise a route	Dependencies and unresolved bridges

Appendix

Table 20: Responsibilities and outputs of research roles and call preparation.

Figure 3: Illustrative support revalidation in RCI: the lemma persists, while a revised candidate requires a new containment proof.

Task or class	Proof scope	Planned tokens (M)
Known-proof S1	Local derivation, certificate, or short key lemma	3.00
Known-proof S2	Single theorem with several connected proof steps	5.00
Known-proof S3	Sharp bound, long dependency chain, or new construction	8.00
C1	Composite optimization: regime analysis and upper/lower bounds	20.00
C2	Finite-chain and statistical lower bounds; sample normalization	8.00
C3	Tree aggregation, accelerated potential, and propagation bound	6.00

Appendix

Table 21: Originally specified generation allocations per task. These planned amounts are distinct from the consumption reported below.

C1: full system, ablations and baselines
Method or case	Tokens (M)
PACE	18.46
A1: Single-pass research–proof	7.96
A2: Fixed-prompt context organization	14.69
A3: Predetermined research sequence	13.64
A4: Proof critique and revision	20.60

Appendix

Table 22: Generation-token consumption for C1–C6, C1 ablations and known-proof tasks.

AI-Assisted Mathematical Discovery

See all 20 papers

May 20, 2026

RMA: Context-Orchestrated Research Math Agents

Long-horizon mathematical reasoning fails less often because a model cannot produce a valid next step than because an agent fails to maintain and expose the right semantic state across many iterations. Left unmanaged, this produces research-level proofs that are locally convincing yet globally incomplete: a key lemma unproved, an assumption unchecked, a citation unsupported, or a computational claim unverified. We present Research Math Agents (RMA), an agentic framework for long-horizon proof development built around a persistent, typed research store and an orchestrator that compiles operation-specific context from that store. The Research Context Orchestrator is the central state-management layer between the persistent research store and each locally scoped proof operation: it retrieves task-relevant artifacts, compiles them into a bounded context, invokes the appropriate operation, and writes the resulting proof edits, issue updates, literature notes, plans, or evaluations back to the store. This process is designed to keep proof revisions, unresolved issues, prior attempts, literature, and evaluations available across rounds while exposing only task-relevant state to each local operation. We evaluate RMA across complementary research-level settings using independent expert evaluation, blind mathematician review, LLM-based benchmark evaluation, and Lean 4 kernel verification. RMA achieves a 42.5% solve rate on the independently evaluated SOOHAK Challenge Hard set, obtains 8 of 10 correct solutions on First Proof B1 and 8 of 10 passing solutions on B2 under human-expert evaluation, and verifies 213 of 300 sampled Research Solved targets in Formal Conjectures with the Lean 4 kernel.

Zelin Zhao, Bo Yuan, Yuchen Zhu +2

Georgia Institute of Technology

LLM Context Management LLM Mathematical Reasoning Autonomous Research Agents Memory-Augmented Language Model Agents

Ask PDF

Jul 30, 2026

MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures

Automatically constructing well-specified and valuable mathematical conjectures remains a central challenge in AI-assisted mathematical discovery. Many existing open problems and conjectures are often too broad, underspecified, or difficult to connect to plausible proof or refutation strategies. We view a mathematical mechanism as a structure or reasoning principle that connects the assumptions of a candidate problem to its target conclusion, such as an inequality, invariant, decomposition, or reduction to an intermediate claim. We present MECA (MEchanism-centered Conjecture Agent), a multi-agent framework that constructs conjectures by jointly developing candidate statements and their supporting mechanisms. Explorer agents propose mechanisms, test how they apply, and revise the candidate conjecture accordingly, while critic agents assess their mathematical validity and research value. Their feedback guides changes to the assumptions, scope, and conclusion. Through this process, MECA transforms broad research directions into precise conjectures with substantive mathematical support while retaining a clearly identified unresolved core. We evaluate MECA in two complementary settings. First, we compare it with a generate-and-revise baseline on reconstructing preselected target-paper conclusions from target-conditioned but article-blind source materials. Second, we construct 100 semi-open problems from literature-derived seeds and existing open problems and evaluate them through independent proof and refutation attempts by automated provers. Our results indicate that mechanism-centered refinement produces well-specified and research-worthy conjectures that remain challenging for current automated provers.

Wentao Long, Yunfei Zhang, Chenyi Li +1

Fudan University · Qingdao University · Peking University

AI Agents for Scientific Discovery Mathematical Reasoning

Ask PDF

May 13, 2026

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics

As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures, an evolving benchmark of currently 2615 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery, and 836 solved problems for proof autoformalization. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged to make new mathematical discoveries, including the resolution of open research conjectures. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.

Moritz Firsching, Paul Lezeau, Salvatore Mercuri +8

Google DeepMind · Imperial College London · Stockholms universitet +1

Mathematical Reasoning Benchmarks Automated Theorem Proving Benchmark Design Autonomous Scientific Discovery Lean Theorem Proving Autoformalization

Ask PDF

Abstract

AI-Assisted Mathematical Discovery

Explore similar work

RMA: Context-Orchestrated Research Math Agents

MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures

Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics