公司概况 - Lanyon AI是一家专注于科学和工程计算AI的基础研究实验室，已从隐身模式中推出[2] - 公司由Jonathan Gorard、Ammar Hakim和James Juno联合创立，三人均曾任职于普林斯顿大学和/或普林斯顿等离子体物理实验室[7][8] - 创始团队拥有超过五十年的综合经验，涵盖应用数学、计算物理学和科学AI领域[8] - Jonathan Gorard是获奖应用数学家，曾与Stephen Wolfram共同创立Wolfram物理项目[8] - Ammar Hakim是世界领先的计算物理学家，在流体力学、核聚变和航空航天工程方面有深厚专长[8] - James Juno是领先的等离子体物理学家，为实验室、空间和天体物理等离子体中最困难的问题开发了尖端方法[8] 融资情况 - Lanyon AI完成了1060万美元的初始融资轮，由Dimension领投，Industrious Ventures参与投资[1][2] - Dimension合伙人兼研究主管Simon Barnett表示支持Lanyon团队将其数十年的形式化方法专业知识转化为神经符号DSL[7] 核心技术 - Lanyon AI正在构建一种全新的科学AI，其正确性有数学证明支持[1] - Lanyon的AI代理可以在几秒钟内模拟复杂物理系统、证明复杂数学定理并发明新算法，仅需GPT-5.6和Fable 5等前沿模型极小部分的token和计算成本[4] - Lanyon生成的任何代码或数据在构造上都是可证明正确的：其生成代码在数学上不可能不符合形式规范[4] - Lanyon采用神经符号方法：让LLM发挥创造力提出有趣想法，同时利用符号方法进行可靠和可预测的扩展[5] - LLM生成规范，然后可靠的符号方法将该规范同时扩展为代码和证明，如果规范无法被严格证明正确，代码就不会生成[5] - Lanyon的形式规范语言高度浓缩且领域特定，因此不仅100%可靠，而且相比现有前沿模型极其快速且低成本[6] 目标市场与应用 - Lanyon AI最初瞄准航空航天工程、空间和大气推进以及核能等关键行业，这些领域需要高精度和可信的计算模拟[7] - 公司针对硬科学：物理学、工程学、GPU内核优化、前沿AI推理以及其他正确性非可选且数学精度至关重要的任务[2] - 形式化验证的高精度模拟对于解决深层次的科学和工程问题至关重要，Lanyon为科技公司解锁创造力并扩展可访问解决方案的范围[7]