AI 中文总结
MECA是一种以机制为中心的多智能体框架，可联合构建候选数学命题及其支撑机制，能生成定义明确且有研究价值的猜想，相关猜想对现有自动证明器仍具挑战性。
AI 中文摘要
自动构建定义明确且有价值的数学猜想，仍是AI辅助数学发现中的核心挑战。许多现有开放问题和猜想往往过于宽泛、定义不明确，或难以与合理的证明或反驳策略建立关联。我们将数学机制视为一种结构或推理原则，它将候选问题的假设与其目标结论（如不等式、不变量、分解或归约为中间命题）关联起来。我们提出MECA（MEchanism-centered Conjecture Agent，以机制为中心的猜想智能体），这是一种多智能体框架，通过联合构建候选命题及其支撑机制来生成猜想。探索智能体提出机制、测试其应用方式，并相应修正候选猜想；而评判智能体则评估这些机制的数学有效性和研究价值。它们的反馈会引导对假设、范围和结论的调整。通过这一过程，MECA将宽泛的研究方向转化为具有实质性数学支撑的精确猜想，同时保留了明确识别的未解决核心。我们在两个互补场景中对MECA进行评估：首先，在从仅受目标条件约束但不依赖目标文章的源材料重构预选目标论文结论的任务上，将其与“生成-修正”基线方法进行比较；其次，我们从文献衍生的种子和现有开放问题中构建100个半开放问题，并通过自动证明器的独立证明与反驳尝试对其进行评估。结果表明，以机制为中心的细化过程能生成定义明确且具有研究价值的猜想，这些猜想对当前自动证明器而言仍具有挑战性。
英文摘要
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.
Comments78 pages, 5 figures. Includes appendices and the full collection of 100 generated conjectures
