FARMS：把计算数学转化为可验证的 AI 知识库
FARMS: A Verifiable Foundation for Automated Computational Science
论文提出 FARMS 框架，把计算数学变成 Lean 验证过的 AI 知识，171 个目标里通过 157 个，单个成本不到 2.3 美元。
FARMS 是一个将计算数学文献转化为 AI 可用计算知识的框架，通过来源准备、可复用表示和语义审查，把形式化陈述与源上下文、算法含义及定量保证关联起来。在随机数值线性代数和数值偏微分方程的 171 个目标中，157 个通过了流水线验收，单个目标的平均估计成本为 0.85 至 2.29 美元。系统用 Lean 检查从显式前提推出的含义，将选定陈述连接到计算技能，文中以热流求解和波响应压缩为例说明。
FARMS: A Verifiable Foundation for Automated Computational Science
Automated computational science could accelerate discovery by selecting, adapting and developing numerical methods. This prospect requires mathematical knowledge that AI systems can interpret and reuse with explicit guarantees. Here we present FARMS, a faithful and efficient foundation that transforms computational mathematics into AI-ready computing knowledge. FARMS connects formal statements to source context, algorithmic meaning and quantitative guarantees through source preparation, reusable representations and semantic review. Across 171 targets in randomized numerical linear algebra and numerical partial differential equations, 157 were accepted by the pipeline, with mean estimated costs of US \$0.85-2.29 per target across sources. Lean-checked implications from explicit source premises connect selected statements to computational skills, illustrated by a heat-flow solve and wave-response compression. FARMS therefore supports an affordable, reusable knowledge foundation for trustworthy automated computational science.