AE Studio 在 Modal 上用进化算法优化 Lean 定理证明

AE Studio 在 Modal 平台上构建了一套基于强化学习的定理证明工作流，利用进化算法（Evolutionary Algorithms）来提升 Lean 证明的生成效率。核心思路是将证明搜索建模为 RL 问题，通过种群迭代和奖励信号引导模型生成更短、更正确的证明路径。

Modal 的弹性计算能力使得大规模并行评估候选证明成为可能，大幅缩短了迭代周期。