AI能写代码，为何还要证明自己？
AI已经能编写代码，可为什么还得接受证明？让AI写几行代码，早就不再新鲜。真正困难的是把它放进包含大量文件、接口和依赖的真实项目后，还能说明“写出来的东西确实达到要求”。UC Berkeley等机构近日推出Vero基准，专门考察这种能力。它把任务置于Lean 4形式化环境中，要求智能体在仓库层面完成两个步骤：先写出实现，再为该实现生成机器可以核验的证明。项目涵盖43个多模块实例，包含743个API和2705条形式化规范，并涉及加密协议、分布式系统等场景。这样的设计看似有些苛刻，却比一段精彩的演示更接近我们
AI推动数学研究迈出关键一步
8月10日这天，Anthropic 发布了一则简短的动态，讲述了一件颇为罕见的事情：一款尚未正式对外公开的研究型 Claude，将黎曼 zeta 函数零点的已知下界，从 41.6% 提升到了 67.2%。这一成果并非为了刷榜或者跑分，而是被正式写入论文之中，经过人类数学家逐行仔细审核，同时借助 Lean 形式化验证工具完成了完整的检验流程。提出这一挑战的是 Anthropic 公司员工 Jarred Sumner，他本人并非数学科班出身。最初，他给模型下达的指令大致意思是：认真尝试一下黎曼猜想。图注：一句
百元成本破解80年数学悬案：AI正在重塑学术研究规则
近期，OpenAI 公布了一则令数学界为之震动的研究成果。其通用推理模型独立推翻了一个悬而未决近八十年的著名猜想——Erdős 平面单位距离问题。这不是辅助人类完成的，也不是检索了已有文献，而是完全自主推理得出的结论。菲尔兹奖得主 Tim Gollars 评价道："若这篇论文以人类名义投向《数学年鉴》，我会毫不犹豫支持发表。"随后 Ethan Mollick 进行了一番测算。基于公开的大模型推理成本数据，解决这个八十年难题所耗费的资源为：电力 0.6–6.3 千瓦时（相当于电动汽车行驶数英里），水资源 3
AI面对黎曼猜想：它还会在哪些地方绊倒
摘要 黎曼猜想（RH）被普遍视为数学史上最重要的悬而未决难题之一。一个半世纪过去，它依旧让所有证明路线无功而返。随着人工智能逐步走入数学推理：能解竞赛题、能做复杂定理的检验、甚至能生成新的猜想——一个顺理成章的追问出现了：AI有没有可能证明黎曼猜想？若有，又需要满足哪些前提？要回答它，我们不得不正视当下AI的短板、数学发现究竟依赖什么、形式化验证在其中扮演的作用，以及在证明能够被“认证”为无误之前必须搭建的巨型知识支架。下面将从三个互相缠绕的方向拆解：当前AI欠缺的关键能力、把解析数论搬进形式系统的浩大工