提出 AIM，一个面向前沿数学研究的大推理模型智能体框架，结合长程探索轨迹和面向验证的机制来处理研究级证明任务。
论文
AIM团队发表或预印的论文。
呈现一个人机协同发现案例：AIM 支持路线探索、定理形成、推导生成与审计流程，并参与推动面向矩阵方程和矩阵函数的符号嵌入量子算法研究。
研究面向开放式数学证明的悲观验证流程：只要任一验证器发现关键错误，就拒绝该证明。
通过均匀化理论案例展示 AIM 辅助推理与人工定向干预如何支持完整数学证明的形成。
提出 FormaRL，一个利用无标注数据、Lean 语法检查和大模型一致性检查提升自动形式化准确率的强化学习框架。