MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 25 of its 45 references that are in the map. First posted on arXiv 30 Jul 2026.
Builds on
25 of 45 references.
References · 25
- 2024The AI Scientist: Towards Fully Automated Open-Ended Scientific Discoverycited by 1,071
- 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 867
- 2020Generative Language Modeling for Automated Theorem Provingcited by 388
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
- 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
- 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
- 2025Mathematical exploration and discovery at scalecited by 77
- 2026Towards Autonomous Mathematics Researchcited by 40
- 2024Reliable Evaluation and Benchmarks for Statement Autoformalizationcited by 32
- 2026M2F: Automated Formalization of Mathematical Literature at Scalecited by 15
- 2026QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problemscited by 13
- 2025LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Provingcited by 8
13 more
- 2026ProofCouncil: An LLM Agent for Solving Open Mathematical Problemscited by 7
- 2025Lemmanaid: Neuro-Symbolic Lemma Conjecturingcited by 6
- 2026Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generationcited by 6
- 2025DeepMath-Creative: A Benchmark for Evaluating Mathematical Creativity of Large Language Modelscited by 5
- 2026MechMath Agent Team: LLM Driven Agents for Mathematical Researchcited by 5
- 2024Automated conjecturing with TxGraffiticited by 4
- 2025A Matter of Interest: Understanding Interestingness of Math Problems in Humans and Language Modelscited by 4
- 2025SITA: A Framework for Structure-to-Instance Theorem Autoformalizationcited by 4
- 2026MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematicscited by 4
- 2026COMPOSE: Composing Future Theorems from Citations and Formal Structurecited by 3
- 2025Conjecturing: An Overlooked Step in Formal Mathematical Reasoningcited by 2
- 2026Can LLM generate interesting mathematical research problems?cited by 2
- 2026OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Provingcited by 1
Built on by
Citing papers per year: 2026: 1.
1 paper.