用AI把数学论文自动转为可编译的Lean代码，提升形式化效率。
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
- 设计工作流驱动的LLM代理，分步完成论文到Lean项目的转化。
- 在2000次API调用内完成两篇未形式化论文的项目构建。
- 适合数学形式化、AI+数学交叉研究者参考。
我们提出并评估了LeanFlow，一个专注于将数学论文转化为可构建Lean项目的LLM智能体系统。现有验证器闭环系统虽能生成大型形式化成果，但其运行机制对完成度、可审计性与效率的影响尚不明确。通过在数论和测度论中两篇未形式化的论文上进行案例研究，采用模型、证明工作流与工具集消融实验，使用Kimi2.6和GPT5.5，记录任务结果、API调用次数、输入与输出词元数量。使用Kimi2.6时，完整工作流在2000次调用预算内完成两个文档级项目，而无队列变体达到预算上限；使用GPT5.5时，所有文档级变体均完成，且完整工作流在两个源上的输入词元成本最低或并列最低。作为补充校准，LeanFlow在RLM25的PFR子集上达到75.7% BEq+，并在GPT5.5实验中解决所有五个ICML 2026 AI for Math TCS挑战项目。
原文摘要 · Abstract (English)
We present and evaluate LeanFlow, an LLM agent system specialized for translating mathematical papers into buildable Lean projects. Recent verifier-in-the-loop systems show that large formal artifacts can be produced, but it remains unclear which runtime mechanisms affect completion, auditability, or efficiency in document-to-project formalization. We study this question through case studies on two previously unformalized mathematical papers in number theory and measure theory, using model, proof-workflow, and toolset ablations with Kimi2.6 and GPT5.5; we report task outcome, API calls, input tokens, and output tokens. With Kimi2.6, the full workflow completes both document-level projects within the 2000-call budget, while no-queue variants reach the budget limit; with GPT5.5, all document-level variants complete, and the full workflow has the lowest or tied-lowest input-token cost on both sources. As complementary calibration, LeanFlow reaches 75.7% BEq+ on the PFR slice of RLM25 and solves all five ICML 2026 AI for Math TCS challenge projects in our GPT5.5 runs.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。