公司融资与估值 - 英伟达参与了Harmonic的C轮融资 此轮融资金额达1.2亿美元 公司估值因此升至14.5亿美元 [4] - 除英伟达外 本轮融资的投资者还包括新进入的爱默生集团 以及现有投资方瑞比特资本 红杉资本 指数创投和凯鹏华盈 [4] - 公司计划将大部分融资用于支付所需的算力资源费用 同时将员工数量从目前的不足30人增加至50到75人 [4] 公司技术与产品 - Harmonic专注于开发用于解决数学问题的人工智能系统 其名为“亚里士多德”的模型不仅能攻克数学难题 在代码编写和芯片设计领域也展现出应用潜力 [3][4] - 公司的技术方案不仅能解决问题 还能以可验证的方式呈现完整的推理过程 这与仅预测下一个token的大型语言模型工作原理不同 [5] - 公司的应用程序编程接口目前仍处于免费测试阶段 暂未确定“亚里士多德”模型的收费模式与付费上线时间 [5] 市场定位与发展前景 - 尽管大型语言模型在数学竞赛中表现出色 但能够对运算结果进行形式化验证的人工智能系统仍存在巨大市场空间 [3] - 公司首席执行官表示 英伟达的支持将助力提升“亚里士多德”的性能 加快数学领域的探索步伐 并推动各行业借助数学人工智能解决关键且高风险的难题 [4] - 创始投资人预见未来的图景是 绝大多数软硬件都将由人工智能生成并经过形式化验证 [5]

文章核心观点 - 文章核心围绕菲尔兹奖得主陶哲轩与其子女Riley Tao的公开对谈展开 对谈主要探讨了人工智能如何与人类科学家协作以加速科学进步 并提出了人机协作的新范式[1][2][24] - 文章同时报道了陶哲轩子女William Tao在2025年宣布选择非二元性别身份并改名为Riley Tao的事件 引发了公众关注[2][3][11] 陶哲轩子女Riley Tao的个人情况 - 陶哲轩与妻子Laura育有一子一女 儿子原名William 女儿名Madeleine[9] - 2025年 William Tao正式宣布选择非二元性别身份 并改名为Riley Tao 陶哲轩对此表示完全尊重与支持[11][13] - Riley Tao是SAIR基金会的主持人 一名大二学生 新型作家 关注科学与人工智能领域[14] - Riley Tao创作并希望推广一部青少年奇幻题材小说 主题涉及跨性别高中生发现自我身份 此外还创作过关于跨纬度生物遭遇职场歧视的短篇科幻小说 显示其对跨性别议题的关注始于2022年[21][23] SAIR项目背景 - SAIR全称为Science & AI Research Foundation 是一个致力于推动科学研究与人工智能协同发展的国际科研机构[27] - 该机构由陶哲轩等科学家领袖共同发起 其成立的部分原因是联邦科研预算的削减[27] - Riley Tao承担了SAIR在媒体上的许多推广工作[28] 人工智能与人类科研协作的新范式 - 陶哲轩将人工智能比喻为喷气式发动机 动力强大但不可靠 需要被装入“飞机”并辅以工程、验证和规则才能安全有效地发挥作用[31][34] - 人工智能正在改变数学研究等领域的游戏规则 陶哲轩本人在研究中频繁使用人工智能进行文献检索、编写代码和运行实验[36] - 新的协作范式是：人工智能负责高速探索和试错 人类则负责最终的判断、抽象与推广[37][38][44] - 人工智能的本质被描述为一种概率性猜测机器 其输出需要经过“过滤系统”的检验 在数学领域 这套系统是形式化验证 此思路可应用于其他科学领域[46][49][51] 人工智能在科研中的具体作用与局限 - 人工智能擅长在庞大的可能空间中进行探索和试错 例如陶哲轩与谷歌DeepMind团队合作 使用AlphaEvolve探索“nodum set”的结构问题 人工智能在参数规模较小的情况下提供了聪明的构造方案[42] - 人类科学家能从人工智能有限的输出案例中理解背后逻辑 并将其抽象、推广为适用于任意大规模参数的通用构造方法 最终完成完全由人类证明的论文[42][45] - 人工智能无法自动证明定理 其真正价值在于承担传统研究中极其昂贵却又重要的探索工作[40][42] 对人类与人工智能关系的展望 - 陶哲轩引用经济学“比较优势”概念 认为未来不是人工智能超越人类 而是各自发挥相对优势进行协作 人工智能的优势在于处理海量信息与跨领域筛选 人类的优势在于跨领域的抽象、迁移与从少数例子中顿悟规律[53] - 人工智能能降低参与高端科研的门槛 将复杂问题拆解为子问题后 普通研究者和业余爱好者均可借助人工智能参与探索或验证[55] - 未来的科研突破可能源于人类智慧、人工智能能力与大规模协作三者的乘积[56] - 陶哲轩对人工智能在国际数学奥赛中夺金持冷静态度 认为一旦“刷爆”基准测试 人工智能可能只是在学习如何应试 而非解决真实、混乱、开放的科研问题 关键是将成熟的人工智能技术打磨成嵌入真实科研流程的工具[57][60][62][63] - 未来十年、二十年的核心议题是人类与人工智能如何根据各自特性进行分工协作[65]

文章核心观点 - 行业在追求重大技术突破时可能忽视通过持续微小改进积累所带来的巨大收益 [3][4] - 通过多个案例表明，在芯片设计等领域，许多小的优化和改进最终能产生显著效果，其长期回报可能优于孤注一掷追求颠覆性变革 [4][5][8] 电子系统级设计发展 - 过去二十年在提高设计和验证抽象层次、软硬件协同设计等ESL目标上进展有限，但当前已能设计出规模和复杂度比以往大数千倍的系统 [3][4] - 尽管在系统性能或功耗分析方面仍存在局限性，但可通过预留裕量、实时测量等方法来弥补 [4] 电源优化策略 - 在典型设计中，通过工具可节省10%到15%的电力，但单次改进可能被忽视，而竞争对手通过在设计过程每一步都注重功耗，积累微小改进从而实现显著的低功耗效果 [5] - 低功耗设计成果可能被劣质软件所抵消，尤其是当软件未能利用硬件为提高能效而内置的功能时 [5] 形式化验证工具的演进 - 形式化验证工具在缺乏重大变革的情况下，从一次版本更新到下一次，工具速度可提升25%甚至翻倍，性能呈指数级增长 [7] - SAT求解器作为形式化验证的基础，在过去20年不断有新的突破性求解器出现，如Chaff、zChaff、MiniSAT，近五年Kissat、MapleSAT等新求解器的结果远超往年 [7] - 尽管大型数据中心提供强大算力，但对形式化证明这类NP难问题的加速效果是线性的，而算法和工程改进带来的提升是指数级的，增加计算能力并不会带来显著差异 [8]

核心观点 - 顾荣辉教授基于形式化验证的数学方法主导Web3安全行业生态 其创立的CertiK已成为全球最大Web3安全公司 估值达20亿美元 市场占有率超过60% [2][5][13] 创始人背景与特质 - 顾荣辉为清华学霸 耶鲁博士 现任哥伦比亚大学全职教授 对数学极度痴迷且天赋过人 高中获数学竞赛国家一等奖 [3] - 在耶鲁读博期间以形式化验证为科研方向 2016年与导师邵中教授共同研发出世界首个被完全形式化验证的操作系统内核CertiKOS 被谷歌红队评为"无懈可击" [5] - 以勤奋著称 经常工作至凌晨四五点 该特质已融入CertiK团队文化 团队成员常凌晨两点开会 [5][8] 技术核心与行业定位 - 形式化验证通过数学方法证明计算机代码和软件系统的安全可靠 虽初期不被学术界看好 但现已成为Web3安全领域核心技术 [4] - Web3安全保障被视为"技术上的王冠" 智能合约一个漏洞可能导致极大损失且不可逆转 [8] - 行业技术发展每三个月更新一次 波动变化极快 类似AI行业 [8] 公司发展里程碑 - 2017年12月创立CertiK 2022年估值达20亿美元 当时顾荣辉33岁 [5] - 已服务超5,000家企业 发现超过15万个安全漏洞 入选三星和Ledger安全名人堂 获苹果6次致谢 [13] - 完成红杉 高瓴等顶级机构多轮融资 审计报告全公开 以透明度独树一帜 [13] 管理方法论与价值观 - 采用优先级区分与接受试错的专注策略 将资源聚焦战略前瞻和P0级事故 次要问题逐步放手 [8] - 核心价值观为"做应该做的事" 即直面客户真实需求而非市场热捧的易实现事项 即使难以实现 [12] - 疫情期间通过线上瑜伽课 邮寄设备 多地年会等创新措施维持团队效率 实现跨时区远程管理 [12] 业务扩展与行业影响 - 从代码安全审计扩展至合规 反洗钱 团队验证等复杂场景 与Web3行业共同成长 [13] - 在2,000多家公司涌入的Web3安全赛道中成为唯一保持增长的头部企业 [13] - 守护对象包括Web3项目及小红书 携程 蚂蚁金服 美团等Web2企业 [13]

核心观点 - Harmonic是一家专注于解决AI幻觉问题的初创公司，其产品Aristotle在数学推理领域实现了零幻觉，通过形式化验证手段确保输出准确性 [5][6][21] - 公司成立仅两年估值接近9亿美元，吸引了红杉资本、凯鹏华盈等顶级投资机构近2亿美元投资 [7][30][34] - 技术核心是基于Lean的交互式定理证明系统，通过严格逻辑约束确保数学推理的准确性 [36][38] - 在MiniF2F测试中达到90%成功率，远超GPT-4等通用AI模型的20-35% [41][42] - 面临DeepSeek、谷歌DeepMind等强劲竞争对手，后者在数学AI领域已有显著成果 [43][46][47] 公司背景 - 由Vlad Tenev和Tudor Achim联合创立，前者是Robinhood CEO（公司估值55亿美元），后者有自动驾驶AI算法开发经验 [9][10][14] - 创始团队具备数学天赋和AI经验，初期使用个人资金启动研发 [11][15] - 公司理念是让AI"会思考、讲真话"，通过严格逻辑约束避免无根据回答 [15] 产品与技术 - Aristotle是首个可进行推理并正式验证的AI产品，在定量推理领域保证零幻觉 [5][21] - 通过Lean证明系统实现：每一步推导需系统认可，错误结论会被立即拒绝 [21][38] - 解决了三大问题：幻觉、推理不清晰、不够严谨，适合金融、医疗等高风险场景 [21] - 在MiniF2F测试集（488道数学题）中创下90%成功率的新纪录 [22][41] - 能自动生成严格数学证明，如2001年国际数学奥林匹克难题 [22][23] 融资与估值 - 种子轮由创始人个人和天使投资人提供 [29] - 2024年9月A轮融资7500万美元，估值3.25亿美元 [30] - 2025年7月B轮融资1亿美元，估值接近9亿美元 [30] - 投资方包括红杉资本、Index Ventures、Kleiner Perkins等顶级机构 [34] 行业竞争 - DeepSeek的Prover-V2模型在MiniF2F测试中达到88.9%通过率 [43] - 谷歌DeepMind的AlphaProof在2024年IMO中获得银牌（6题解出4题） [46] - OpenAI新模型在IMO2025斩获金牌（6题解出5道） [49] - 竞争对手普遍拥有大模型生态支持，如DeepSeek-V3、Gemini等 [51] 市场定位 - 瞄准B端精密场景（金融建模、科学推理等）对极低容错率的需求 [19] - 计划发布企业API和消费者网络应用 [24] - 可能选择被大厂收购作为退出路径，成为基础模型技术生态的一环 [51]

公司背景与创始人 - 公司Harmonic专注于解决AI幻觉问题 开发零幻觉AI模型Aristotle [3] - 联合创始人Vlad Tenev为数学背景 曾创立估值55亿美元的金融科技公司Robinhood [7][8][11] - 联合创始人Tudor Achim为计算机科学专家 曾创立自动驾驶公司Helm.ai并融资1.02亿美元 [12] - 公司成立初期使用Vlad Tenev个人资金启动 [11] 技术突破与产品特性 - Aristotle模型通过Lean证明系统实现数学推理零幻觉 每一步推导需经系统验证 [19][31][33] - 模型在MiniF2F测试集（488道数学题）中达成90%通过率 远超GPT-4的20-35% [37][38] - 产品支持自然语言输入 自动生成严格数学证明并提供步骤解释 [18][20][21] - 宣称在IMO2025竞赛中获得金牌成绩 [3] 融资与估值 - 公司两年内估值从零升至接近9亿美元 [5][27] - A轮融资（2024年9月）获7500万美元 估值3.25亿美元 [27] - B轮融资（2025年7月）获1亿美元 估值接近9亿美元 [27] - 投资方包括红杉资本、Index Ventures、Kleiner Perkins及Paradigm等顶级机构 [28][29] 行业竞争格局 - 竞争对手DeepSeek的Prover-V2模型在MiniF2F测试中达88.9%通过率 [41] - 谷歌DeepMind的AlphaProof在2024年IMO获银牌（解出4/6题） [44] - OpenAI等大厂通过自然语言路径仍存在高幻觉率问题 [4][24] 商业模式与战略方向 - 公司推出iOS/Android聊天机器人测试版及企业API接口 [3][22] - 目标市场包括金融建模、科学推理等低容错率B端领域 [17] - 技术路径依赖形式化验证 与主流非形式化路径形成差异 [4][35] - 潜在发展路径包括被大厂收购以整合技术生态 [46]

Harmonic AI融资与估值 - 人工智能初创公司Harmonic AI完成1亿美元B轮融资 由Kleiner Perkins领投 红杉资本 Index Ventures和Paradigm跟投 [1] - 本轮融资后公司估值达8 75亿美元 略低于10亿美元独角兽门槛 创始人称此为有意为之的选择 [1] - 公司此前已从红杉资本和Index Ventures获得7500万美元融资 累计融资额达1 75亿美元 [1] 公司背景与团队 - 公司由Robinhood Markets CEO弗拉德·特涅夫与都铎·阿基姆于2023年联合创立 总部位于加州帕洛阿尔托 [1] - CEO都铎·阿基姆曾领导自动驾驶初创公司Helm ai 特涅夫担任非执行董事长 [1] - 公司专注于开发解决复杂数学问题的人工智能系统 目标打造"数学超级智能" [1] 技术方向与产品规划 - 旗舰AI模型Aristotle计划2025年向研究人员和公众开放 [2] - 短期目标为开发数学解题能力超越人类水平的AI 长期目标攻克数学领域未解难题并拓展至物理学和计算机科学 [2] - 采用形式化验证技术消除AI幻觉问题 确保模型输出和推理步骤可验证 [2][3] - 公司认为以数学为核心的策略将优于现有大型语言模型 后者普遍存在数学能力不足缺陷 [2] 创始人观点 - 特涅夫强调不应追求估值最大化 公司主动控制估值低于独角兽门槛 [1][3] - 提出形式化验证将成为未来AI模型主流构建方式 [3]

陶哲轩实分析教材形式化项目 核心观点 - 陶哲轩为《Analysis I》教材创建Lean配套项目 将教材中的定义、定理和练习转换为Lean可交互形式 为学生提供新型学习工具[1][2] - 项目采用渐进式策略 前期独立构建数学结构 后期逐步迁移至标准数学库Mathlib 兼具教材辅助和工具入门双重功能[5] - 形式化内容严格遵循原书结构 但刻意避免直接引用原文 定位为注解式辅助资料而非替代品[4] 项目技术细节 - 使用Lean依赖类型理论 特别利用其出色的商类型支持 与教材采用的朴素类型理论高度兼容[2] - 当前已完成部分章节形式化 采用"先独立后迁移"模式 例如第2章先自定义自然数体系 再建立与Mathlib标准体系的同构关系[5] - 习题部分以"sorry"占位符呈现 不提供官方解答 鼓励用户自行完成并创建项目副本[2][4] 教育应用价值 - 为数学系学生提供即时反馈机制 错误证明无法通过编译 显著提升学习效率[10] - 架设教材与Mathlib工具间的桥梁 降低形式化验证的学习门槛[9] - 开源项目允许自由协作 陶哲轩本人将持续收集用户反馈以优化项目[7] 社区反响 - 数学爱好者高度认可该项目价值 认为其首次实现编程式严谨构建数学体系的教学目标[9] - 教育工作者期待未来结合LLM技术 使Lean编译器能提供类似Rust的指导性错误修正建议[10]

文章核心观点 以太坊基金会公布 2025 年第一季度研究资助名单，CertiK 获两项源于 zkEVM 形式化验证竞赛的资助，彰显其在零知识证明系统形式化验证领域的全球技术领导力，其工作将为以太坊生态系统的可扩展性和安全性提供保障并为其他区块链项目树立标杆 [1][3] 公司情况 - CertiK 获以太坊基金会 2025 年第一季度两项研究资助，源于 zkEVM 形式化验证竞赛 [1] - CertiK 的“先进形式化验证”技术相比传统方案有四大突破，适合处理复杂零知识证明系统 [1][2] - CertiK 自创立以形式化验证为核心技术，依托学术成果为 Web3 项目提供安全服务 [1] - CertiK 去年完成 zkWasm 电路的首次完整形式化验证 [2] - CertiK 的形式化验证技术在多个 Web3 顶级项目和基础设施中广泛应用 [2] 行业情况 - zkEVM 通过零知识证明实现以太坊可扩展性，但面临安全风险，形式化验证是确保其正确性和安全性的关键工具 [2] - 随着区块链技术发展，特别是零知识证明系统广泛应用，形式化验证将成确保系统安全和可靠性的关键工具 [3]