Lanyon AI 的 CEO：AI 在代码和数学上起飞是因为有验证器，物理没有，所以先造一门给 AI 用的科学推理语言

验证器决定了 AI 在哪里先起飞

Gorard 说，近两年的能力提升主要来自后训练和强化学习环境，也就是验证器有多好。软件有编译器和类型检查，数学有 Lean 这类证明助手，所以编码和数学先起飞；物理、化学、生物、工程“现在没有”。他把根源追到希尔伯特：判定问题催生了计算理论，也就是数学推理的形式语言；希尔伯特对物理提过同样的问题，至今没有解。他提到图灵唯一的学生 Robin Gandy 的博士论文是最接近的一次尝试，没有走通。

“We want to make physics executable in the same way that software is executable and that now increasingly mathematics is executable.”Jonathan Gorard

物理推理有三层，实验那层最难

第一层是数学上自洽，难度已经不低于形式化数学；第二层是和已有物理原理相容（能量守恒、热力学、协变性），这里有大量只在某些范围成立的启发式，他称之为“更模糊的推理”，还没有被正确地形式化；第三层是和物理现实相符，“远远超过前两层”：任何观测都带着理论，他举“探测到一个粒子”背后有 20 到 50 层理论假设。Lanyon 先做前两层，刚招了一位下几周入职的人去做实验装置的接入。

产品：接在大语言模型上的科学推理语言

现在的 Lanyon 智能体是一个包在 harness 里的大语言模型，但它不用英文或 Lean，而是用一门紧凑的、为物理和科学优化的专用语言来推理；他的比喻是“物理的类型系统”，能检查能量守恒、热力学稳定性、收敛阶。语言可以确定性地展开成实现代码和证明，所以不会出现“代码和证明对不上”的误形式化。他说公司不靠算力和后训练去和大实验室竞争，主要做语言，不做模型；用扩散模型替换里面的大语言模型做过有限的实验，性能下降“不少”，但没有预想的多。

可读性和表达力要取舍

把 AI 限制在少数人能懂的基本元素里，输出很容易读，但推理可能长到十万步，人脑装不下；语言越有表达力，离人能理解的就越远。Lanyon 想找中间点，不全押能力，也不要求样样都能让人审计。他认为 AI 解决问题和把理解传给人是两回事，自己读论文必须亲手推一遍才算懂，所以不赞成用大语言模型替代这一步。

他为什么离开学界

他说转折点是 2026 年 3 月 Math Inc. 公布了用 AI 全自动形式化的 Maryna Viazovska 球体堆积证明；一月时他以为这最早要到 2027 年底。他由此担心：基础研究过去靠“科学作为产品”（治癌、聚变）来为“科学作为过程”（好奇心驱动）辩护，AI 一旦能做产品，过程就没人资助了。他和合伙人把这个想法当学术项目申请经费，“要么没回音要么被拒”，六月初决定成立公司（官网把出隐身标在七月）。他看到的同行反应没有清晰规律，只有微弱的年龄相关：最年轻的和最资深的接受得快，中间一代最倾向于说它不行。

“The timelines were completely wrong.”Jonathan Gorard

物理学家留下什么

他同意主持人的看法：做实验的物理学家眼下不会被取代，原因是造东西有惯性。他说自己在为一部分物理哀悼，但认为学科由方法和动机定义，不由内容定义：做物理的细节会被 AI 彻底改变，“想建立稳健的世界模型”这一动机不会变。他对公司的期望之一是自动发现新的“描述语言”，让人像用哈密顿力学那样用得上，自己留下好玩的部分去玩。