核心技术架构 - 系统基于Lean定理证明器构建强化学习环境，将数学证明过程转化为游戏，通过选择策略推进证明[6] - 采用30亿参数的编码器-解码器transformer模型作为核心证明网络，同时输出策略建议和完成证明所需步数估计[8][9] - 搜索算法采用受AlphaZero启发的树搜索，并引入AND-OR树结构处理多个独立子目标，加入渐进采样机制探索多样证明策略[10] 训练方法与数据 - 预训练使用约3000亿个token的代码和数学文本，随后用Mathlib库中约30万个人工编写证明进行微调[11] - 通过基于Gemini 1.5 Pro的翻译系统，从约100万道自然语言数学题生成约8000万道形式化问题，远超现有数据集[11] - 主强化学习训练阶段消耗约8万TPU天计算资源，通过不断尝试证明自动生成的命题来更新神经网络[11][12] 测试时强化学习机制 - 面对困难目标问题时，变体生成器会围绕该题产生约40万个相关变体，创建小型专用数据集[16] - 变体包含简化特殊情况、推广到更一般形式等数学直觉，系统启动独立AlphaZero式学习过程专门训练[17] - 该机制可并行处理多个目标问题，每个问题都有专属的变体课程和学习进程[17] IMO比赛表现 - 在2024年IMO上成功解决代数和数论的三道题，包括最难的P6题，该题609名参赛者中仅5人完全解出[17][19] - 每道题的测试时强化学习过程需要2-3天计算时间，最终成绩达到金牌水平[17][19][20] - 比赛期间团队规模较小，大部分时间约10人，临近比赛才扩充，核心突破来自IMO金牌得主Miklós Horváth的变体生成方法[3] 应用反馈与局限性 - 数学家试用发现系统擅长找出反例，能快速指出陈述问题，有助于迭代得到正确形式化陈述[23] - 面对充满"定制化定义"的证明时遇到困难，在Lean中已有概念成熟的数学子领域性能更佳[24] - 依赖持续演进的Lean定理证明器造成不稳定环境，且独特数学题数量有限，生成自有问题是未来拓展方向[24]