直接面对真实 Agent 任务
让智能体进化
围绕智能体强化学习与可验证科学智能，构建从真实反馈、形式化验证到持续演化的研究能力。
真实反馈连续任务、轨迹与评测
持续进化让技能与策略不断迭代
机器验证让推理结论经得起检查
01 / 强化学习
让智能体在真实反馈中
持续进化
以非侵入式环境接入、真实轨迹评测与持续训练闭环，构建可运行、可复用的 Agentic RL 基础设施。
- 真实智能体任务直接接入工具、应用与环境
- 轨迹与评测沉淀真实交互、奖励与反馈
- 学习与进化训练 Skills、Harness 与策略
- 重新部署让能力回流到任务中验证
真实任务反馈 · 策略持续学习
把有效经验转化为能力
在任务间学习最优分配
02 / 可验证科学智能
从 AI4Math 出发
将大模型、智能体与 Lean 形式化验证结合：系统提出思路、构造证明，并在机器校验反馈中持续修正与积累。
可验证推理工作流
提出思路 → 形式化 → Lean 校验 → 证明资产
从竞赛试验走向可复用基础设施
- 01AI4Math 竞赛试验场
围绕代数方程隐含任务，探索证明搜索、反例构造与 Lean 4 校验。
- 02Lean 证明资产库
沉淀证明与中间引理，面向大规模存储、检索与复用。
- 03可验证推理智能体
让模型提路线、引擎填实步骤，再由 Lean 进行最终机器校验。