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

arXiv: https://arxiv.org/abs/2607.27709 · HTML: https://mlsanity.com/paper/2607.27709/

## Key facts

- Cited by 1 papers 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 (most cited first, 25 of 25)

- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Mathematical exploration and discovery at scale](https://mlsanity.com/paper/2511.02864/) (2025)
- [Towards Autonomous Mathematics Research](https://mlsanity.com/paper/2602.10177/) (2026)
- [Reliable Evaluation and Benchmarks for Statement Autoformalization](https://mlsanity.com/paper/2406.07222/) (2024)
- [M2F: Automated Formalization of Mathematical Literature at Scale](https://mlsanity.com/paper/2602.17016/) (2026)
- [QED: An Open-Source Multi-Agent System for Generating Mathematical Proofs on Open Problems](https://mlsanity.com/paper/2604.24021/) (2026)
- [LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving](https://mlsanity.com/paper/2506.22005/) (2025)
- [ProofCouncil: An LLM Agent for Solving Open Mathematical Problems](https://mlsanity.com/paper/2607.09474/) (2026)
- [Lemmanaid: Neuro-Symbolic Lemma Conjecturing](https://mlsanity.com/paper/2504.04942/) (2025)
- [Moonshine: An Autonomous Mathematical Research Agent Centered on Conjecture Generation](https://mlsanity.com/paper/2606.10806/) (2026)
- [DeepMath-Creative: A Benchmark for Evaluating Mathematical Creativity of Large Language Models](https://mlsanity.com/paper/2505.08744/) (2025)
- [MechMath Agent Team: LLM Driven Agents for Mathematical Research](https://mlsanity.com/paper/2607.04394/) (2026)
- [Automated conjecturing with TxGraffiti](https://mlsanity.com/paper/2409.19379/) (2024)
- [A Matter of Interest: Understanding Interestingness of Math Problems in Humans and Language Models](https://mlsanity.com/paper/2511.08548/) (2025)
- [SITA: A Framework for Structure-to-Instance Theorem Autoformalization](https://mlsanity.com/paper/2511.10356/) (2025)
- [MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics](https://mlsanity.com/paper/2602.02561/) (2026)
- [COMPOSE: Composing Future Theorems from Citations and Formal Structure](https://mlsanity.com/paper/2605.30333/) (2026)
- [Conjecturing: An Overlooked Step in Formal Mathematical Reasoning](https://mlsanity.com/paper/2510.11986/) (2025)
- [Can LLM generate interesting mathematical research problems?](https://mlsanity.com/paper/2603.18813/) (2026)
- [OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving](https://mlsanity.com/paper/2604.23712/) (2026)

## Built on by (most cited first, 1 of 1)

- [LANTERN: Illuminating Hidden Mathematical Knowledge in Language Models](https://mlsanity.com/paper/2609.32264/) (2026)

## 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.