AI自主提出并证明数学新问题，全程可追溯可验证。
Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research
- 用可执行有向无环图组织证明步骤，每步独立验证并生成证书。
- 解决带切换拓扑的延迟异构网络同步问题，排除奇点行为。
- 适合数学研究自动化、形式化验证方向的学者参考。
Andy 是一个自主数学研究智能体，能将数学问题转化为可追溯的证明。它可求解或验证提交的问题，通过研究价值评估机制提出基于文献的新问题，并完成证明构建与最终验证。系统以可执行有向无环图（DAG）组织证明步骤，独立验证每一步并绑定结果至证书，保留已验证成果且接口不变时支持局部修复，完整记录从问题提出到最终证明的全过程路径。该系统分离证明生成与正确性评估，可获取、保留、检索和复用已有成果。从自触发脉冲共识结果出发，Andy 提出针对具有切换通信拓扑的延迟异构网络的全局指数领导者-跟随者同步问题。所提混合控制结合自触发脉冲与执行延迟及恢复窗口内的连续反馈。每次延迟脉冲后，反馈消除延迟误差通道，直至脉冲前历史离开活跃延迟区间。建立了全局指数同步的充分条件，排除了两种时间序列的奇点行为，并通过数值例子验证结果。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。