Lanyon AI 披露 1060 万美元融资轮，旨在让物理代码自证其正确性

Why it matters

Lanyon AI is betting that scientific AI will be sold on verifiability rather than fluency. The hard part is proving that a formal specification reflects what an engineer intended.

Jonathan Gorard (@getjonwithit)，一位曾在 Wolfram Research 和 Princeton 工作的应用数学家，正走一条更狭窄的路径进入 AI 生成代码领域：让软件证明它确实实现了其形式规范所述的内容。

Lanyon AI，由 Gorard 与计算物理学家 Ammar Hakim (@minmodammar) 和 James "Jimmy" Juno (@JunoRavin) 共同创立，在 8 月 17 日的新闻稿 中表示，其在 7 月完成了初始 1060 万美元的融资后已脱离隐身状态。根据 Lanyon AI 的公告，Dimension 主导了本轮融资，Industrious Ventures 和天使投资人 Siqi Chen 参与了投资。

这家位于新泽西州 Princeton 的实验室正在构建一个名为 Lanyon 的 AI 代理，用于生成科学仿真代码及随附的数学证明。Lanyon AI 最初将该系统推向航空航天、推进、核能等领域——在这些领域，如果工程师无法验证底层计算，表面上看似合理的答案几乎没有用处。

Industrious Ventures 在其投资公告中表示，Gorard、Hakim 和 Juno 在 Princeton Plasma Physics Laboratory 工作期间相识。他们的研究涵盖融合反应堆和黑洞周围的等离子体环境。普林斯顿的记录显示，Gorard 于 2024 年加入该校的研究软件工程小组，参与由 Hakim 领导的多物理场仿真框架 Gkeyll 的工作。

Gorard 拥有 University of Cambridge 的科学计算 MPhil 学位，曾在 Cardiff University、Wolfram Research 和 Wolfram Institute 任职。Lanyon AI 表示，他曾与 Stephen Wolfram 一起参与创立 Wolfram Physics Project。Hakim 的工作涉及流体力学、核聚变和航空航天工程，而 Juno 则专注于实验室、空间和天体物理等离子体的研究。

这些背景早于募资宣讲。Gorard 和 Hakim 在 2025 年发表了一个针对双曲型偏微分方程求解器的形式化验证管道。该三人组于 2026 年 2 月随后发布了 BEACONS，这是一个用于生成神经求解器的框架，提供关于收敛性、稳定性和守恒性等性质的机器可检验保障。

Lanyon 将创造力与验证分离

Lanyon AI 的架构将不同任务分配给语言模型和符号软件。一个大型语言模型 (LLM) 在领域专用的形式语言中提出规范。然后，确定性系统将该规范展开为可执行的 C 代码和 Lean（一个定理证明语言）中的证明。Lanyon AI 表示，如果证明过程失败，则不会生成实现代码。

这种区分很重要，因为要求语言模型先写代码再单独生成证明会产生另一个失败点：证明可能验证的是与代码实现不同的规范。Lanyon AI 的系统则从同一形式化源导出实现和证明。

这种设计支持的保障比 Lanyon AI 最广泛的说法可能暗示的要窄。在其 7 月发布文章 中，Lanyon AI 最初将该代理描述为在数学上不可能出错。一个脚注对该断言作了限定：Lanyon AI 保证实现与形式规范相匹配，但确定规范是否反映了用户的自然语言意图仍然是一个开放的研究问题。

因此，实际风险随之上移。生成的代码可以忠实地实现一个并未表达工程师真实意图的规范。Lanyon AI 的技术论点依赖于在保持形式化保障（使该产品有别于传统编码代理）的同时缩小这一语义差距。

Lanyon AI 已开始通过其 GitHub 组织 发布示例，包括针对 Maxwell's equations、compressible Euler equations、advection-diffusion systems 和 electrostatic Vlasov equations 的形式化验证求解器。仓库提供可检查的代码和 Lean 证明，尽管 Lanyon AI 更广泛的性能和成本比较仍基于由 Lanyon AI 自行生成的基准。

投资者覆盖研究与工业销售

投资者阵容与创始人的问题高度契合。Dimension 将自己描述为一家以研究为导向、专注于科学与计算的投资公司。Industrious Ventures 在航空航天、能源、制造、国家安全及 Lanyon AI 希望进入的其他工业领域进行投资。

Gorard 写道，创始人是“刚出学术界的三个书呆子理论家”，他们需要接触航空航天、核能和国防领域的客户。Industrious Ventures 提供了这些关系网络。Dimension 则在创始人围绕其形式方法工作开发商业产品的同时，给予 Lanyon AI 作为研究实验室运作的空间。

Chen 提供了最早的资金。Gorard 表示，Chen 的投资支付了 Lanyon AI 在接下来的募资过程中用于首个办公室、计算机和法律顾问的费用。

这笔 1060 万美元的资金让创始人有时间将多年的研究转化为生产级软件，并寻找愿意将 AI 生成的仿真代码应用于昂贵物理系统附近的买家。Lanyon AI 已经展示了证明可以与代码同时生成。其商业检验在于工程师是否足够信任规范流程并使用其输出。