arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~

Andy:用于严谨证明与自主研究的数学智能体

Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research

Zi'an Wang

arXiv 2608.15052首次发表:更新:

发表机构

School of Mathematical Sciences, Tongji University; Key Laboratory of Intelligent Computing and Applications (Tongji University)(同济大学数学科学学院; 同济大学智能计算与应用重点实验室)

机构由 AI 辅助整理,请以论文原文为准。

AI 中文总结

该研究提出自主数学智能体Andy,以自触发脉冲共识的已发表结果为基础,构建混合控制方案并验证同步条件,展现其提出问题、开发并验证严谨证明的能力。

AI 中文摘要

Andy是一款自主数学研究智能体,可解决并验证提交的问题、提出新的研究问题并构建严谨证明。它将证明生成与正确性评估分离开,支持知识获取、针对性修正及多阶段验证。本文以一个已发表的自触发脉冲共识研究结果为起点,阐述其工作流程:Andy针对带切换通信拓扑的时滞异质网络,提出全局指数型主从同步问题;所提出的混合控制将自触发脉冲与时滞、恢复阶段的连续反馈相结合,在每次时滞脉冲后,该反馈会在恢复窗口内抵消时滞误差通道;研究建立了全局指数同步的充分条件,且采样序列与脉冲序列均排除了芝诺(Zeno)行为;数值示例验证了该结果,此案例证明Andy具备从现有成果中学习、提出有意义研究问题及开发并验证严谨证明的能力。

英文摘要

Andy is an autonomous mathematical research agent that turns a mathematical problem into a traceable proof. It solves or verifies a submitted problem, formulates a literature-grounded new problem through a research-value gate, and carries it through proof construction and final verification. It organizes proof steps in an executable DAG, verifies each step independently and binds the result to a certificate, retains verified work whose interfaces remain unchanged during local repair, and records the full path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. Starting from a self-triggered impulsive consensus result, Andy formulates a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The proposed hybrid control combines self-triggered impulses with execution delay and continuous feedback over a recovery window. After each delayed impulse, the feedback cancels the delayed error channel until the pre-impulse history leaves the active delay interval. Sufficient conditions for global exponential synchronization are established, Zeno behavior is excluded for both timing sequences, and a numerical example illustrates the result.

Comments20 pages, 4 figures, 3 tables, and 3 algorithms. Research logs, reports, and simulation code are available at https://github.com/mowaiwaim/Andy

论文原文

arXiv 摘要页 · PDF 原文 · HTML 原文

↑