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

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

Specula 是一个智能体式系统，目标是自动化软件缺陷发现流程。它能够从代码中自动推导 TLA+ 规范，通过轨迹验证检查代码与规范之间的一致性，并对规范进行模型检查以发现并发缺陷；随后，它还会编写具有精确时序的集...

Anthropic公司研发的AI模型Claude在一个尚未正式发布的版本中，于黎曼猜想相关的核心问题上取得了令人瞩目的进展。黎曼猜想作为数学界最负盛名的未解难题之一，其核心在于黎曼zeta函数非平凡零点的分布规律，与素数...

上周刚获得数学界最高荣誉菲尔兹奖的加拿大数学家Jacob Tsimerman，已从多伦多大学申请长期休假，转而加入OpenAI，专注于人工智能安全研究。这一动向不仅展现了基础科学前沿与AI产业的深度交融，也再次印证了AI安全...

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

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

硅谷初创公司Axiom在成立仅一年、团队约20人规模之际，成功完成了由Menlo Ventures领投的2亿美元A轮融资，估值高达16亿美元。该公司致力于开发名为“Verified AI”的系统，其核心创新在于利用形式化验证技术，确保AI生...