公司业务与技术突破 - 新公司Math Inc致力于通过自动形式化技术打造可验证超级智能 专注于将人类数学成果转化为机器可验证代码[2][4] - 核心产品Gauss智能体实现超10小时自主运行 在三周内完成强素数定理形式化 而人类专家团队此前投入18个月仅取得阶段性进展[4][5] - 生成约2.5万行Lean代码 包含1000余个定理与定义 单次迭代可自主完成95%命题形式化与证明工作[5][6][8] 技术实现与基础设施 - 基于Morph Labs开发的RL基础设施与Trinity环境 支持数千个并发智能体 每个智能体拥有独立Lean运行时 占用数TB集群内存[8] - 采用Morph Cloud的Infinibranch技术解决大规模Lean验证环境的系统工程挑战[8] 行业影响与学术认可 - 完成复分析领域关键缺失成果的形式化 为以往"难以触及"的研究方向扫清障碍[5] - 数论专家Jared Duker Lichtman评价其开创"人机协作新范式" 物理学家Jose Ali Vivas与计算机教授Pedro Domingos均高度认可其技术突破[10] - 形式验证与人工智能结合被视为绝配组合 预计未来12个月内将形式化代码总量提升2-3个数量级[10] 创始人背景与历史成就 - 创始人Christian Szegedy为xAI前联合创始人 Morph Labs前首席科学家 曾领导谷歌N2Formal团队[12] - 2015年与Sergey Ioffe共同提出批归一化(BatchNorm)技术 彻底改变深度学习训练方式 获ICML 2025时间检验奖[13] - 在xAI期间曾就LLM推理能力与LeCun展开公开辩论 强调强化学习反馈循环对数学推理的重要性[12]