近日，Axiom 宣布已完成对整个 Stacks Project 的 Lean 形式化。Stacks Project 是现代代数几何领域的重要开源参考文献，系统整理了概形、层、上同调等核心理论，是当代数学研究的基础性资源。此次发布将这一长期积...

近日，Axiom Math发布了有限单群分类定理（CFSG）的首个完整计算机检查证明，这是数学史上的一项重大里程碑。CFSG被公认为人类写过的最长数学证明，原始证明横跨约15000页、500多篇论文，由约100位数学家共同完成。A...

OpenAI 宣布了三项由模型生成的研究结果，分别涉及调和分析、计算复杂性理论和量子场论。其中最引人关注的是在复杂性理论中，模型给出了一个经 Lean 验证的证明，表明长期存在的指数时间假说（Exponential Time Hypo...

OpenAI宣布其内部AI系统完成了对纳维-斯托克斯存在性与光滑性问题的证明，这一难题已有约90年历史，并位列克雷数学研究所七大千禧年大奖难题。该模型的研究结论是，光滑的三维流体动力学可以发展出有限时间奇点，意...

Anthropic宣布其AI系统Claude在Lean证明助手中仅用11天，就完成了费马大定理的首个完整计算机可验证证明。该定理由Andrew Wiles于1995年首次给出手工证明，其形式化验证长期被视为极其复杂的工作。Claude生成的证明...

在依赖类型语言的世界里，强大的类型系统往往意味着沉重的证明负担——开发者可能需要花费数小时才能发现要证明的命题根本就是错误的。这种高昂的认知开销使依赖类型编程长期停留在小众领域。如今，这一局面正在被打破...

由企业软件巨头Apptio联合创始人Sunny Gupta等人创办的AI初创公司Thira正式走出隐秘模式，宣布获得由老牌风投Madrona领投的2100万美元种子轮融资。Thira聚焦利用AI代理（AI Agents）接手IT支持、财务对账等繁琐的企...

谷歌DeepMind团队推出新系统AlphaProof Nexus，在未依赖公开发表或训练集中可见的标准解法的情况下，自主解决了353个公开埃尔德什（Erdős）问题中的9道，其中有两道难题甚至困扰了数学界56年之久。值得一提的是，每...