作者丨黄艳冰
雷峰网·鲸犀独家获悉， AxiomMath 伦敦团队前 1 号员工兼形式化验证负责人张巨见已开启创业，于 2026 年 7 月创立北京有理数科技有限公司（下文简称有理数），切入芯片形式化验证方向。
据悉，有理数已完成种子轮融资，即将开始新一轮融资。
有理数团队由世界级数学极客带队，创始人张巨见博士毕业于帝国理工学院，导师 Kevin Buzzard 为全球形式化数学运动的领军人物。张巨见深度参与形式化数学基础设施 Mathlib 的开发，不仅最早参与 Mathlib 开发，同时是贡献度最高的华人开发者之一。此后，张巨见加入AI数学公司 AxiomMath，其联合开发的 AxiomProver已自主证明了多个开放的数学问题，相关成果已陆续发表于同行评审期刊；此后张巨见也联合负责公司内软件和硬件的相关工作。
联合创始人刘俊杞本科毕业于天津大学数学学院，目前是中国科学院数学博士在读。刘俊杞先后在阶跃星辰、月之暗面进行 AI4MATH 研究，并在非营利 AI4Math 组织 Project Numina 担任形式化团队负责人。他也是 Kimina-Prover 的核心贡献者以及开源项目 Numina-Lean-Agent 的共同第一作者，参与包括菲尔兹奖成果三维挂谷猜想的形式化验证等多个项目。
雷峰网·鲸犀获悉，该团队阵容豪华，除了两大联创外，研究班底来自中国科学院数学与系统科学研究院、Project Numina（开源数学 AI 顶尖组织）等；产业班底则有来自 ARM、Intel 的一线芯片工程师。这样的组合在业内极为稀缺。全球 Mathlib 的贡献者不过数百人，而能同时打通形式化数学、AI 定理证明与芯片验证三个领域的人才更是凤毛麟角。团队成员开发的 Agent 系统近日在 CCF 中国软件大会第二届定理证明竞赛人与AI协作赛道决赛中获得冠军。
方向上，团队为突破现有抽样测试的手段，采用 AI 结合形式化数学进行全量证明，可保证结果绝对正确，因为只有数学无法说谎。这一路径对传统芯片验证而言，近乎一次“降维打击”，可从容面对天文数字的状态空间。过去类似手段因依赖顶尖专家手工完成，无法大规模的铺开。如今验证已占到芯片研发周期的一半左右，是行业最大的瓶颈之一。
与此同时，谷歌、微软已有约三成新代码由 AI 生成，谁来验证 AI 正成为新的产业刚需。OpenAI、Google DeepMind 等前沿实验室也纷纷用 Lean 为 AI 的产出背书。
接近该团队的人士告诉鲸犀，目前技术已经跑通原型，有能力针对十几万行的芯片代码做出现有EDA工具无法判断的断言，团队现阶段正和部分芯片客户共建标杆，将“验证服务”商业化。
有理数后续融资及产品进展，雷峰网·鲸犀将持续关注，欢迎添加作者微信 frenchfries0016 交流。
