AI加速代码编写，但正确性验证成为瓶颈。文章介绍Go形式化验证工具Gobra及其底层Viper，通过前置条件、后置条件、循环不变量和权限模型，将程序性质转化为机器可检查的证明义务，并以求和算法演示。形式化验证不等于零缺陷，规范本身可能写错。AI Agent可生成候选规范、修复证明失败，但结论须由验证器给出，而非由另一个大模型判断。

陶哲轩博客客座文章指出，OpenAI在GitHub发布的数学文稿难以理解且引用不全。数学社区因此发起修订项目，邀请学生、博士后、教授及爱好者共同改进，并提供可浏览网页；成员还可发邮件申请担任管理员或审稿人，按分类参与审阅。

陶哲轩介绍，IAS数学学院今年在会员项目申请中新增说明：鉴于当前申请压力大，允许申请人提交仅基于已完成研究的研究陈述，建议聚焦少数（通常不超过三项）精选项目而非罗列全部工作。他预计其他院系和机构今年也会采取类似指引，并提到理论计算机科学领域工作组近期也有相似建议。

文章从“数学是年轻人的游戏”切入，指出AI正引发数学空前剧变。作者认为机器虽已能证明重要结果，但数学的核心价值在于人类理解，而非罗列真命题；AI还可推动数学与物理重新结合，并严格化物理推导。作者批评AI公司无偿攫取数学家的数据与未公开想法，存在利益冲突，呼吁保护数据、限制AI公司、降低前沿模型使用门槛，并建立奖励理解而非资源的新贡献认定体系。

陶哲轩提出“Math 2.0”实验挑战：利用AI从排除Landau–Siegel零点的各类新论证中，推导假想第十个判别式（Heegner数）的有效上界，并尽量优化常数，且不使用Heegner方法。该问题已解决，无干扰研究之虞。他邀请读者提交可验证的界，允许使用AI但须披露，鼓励协作而非竞赛，重视论证的简洁性与可检验性。

陶哲轩博客刊载Francesco Maggi客座文章，讨论大语言模型对数学与科学的影响。作者认为LLM已能生成重要证明，但人类理解仍是数学的核心，若知识脱离人类理解将走向“黑暗时代”。他提出：LLM擅长重组已有文献却难以完成“数学化”；数学进步不能以解题清单衡量；署名、同行评审与人才培养面临挑战；前沿模型被少数公司控制存在风险。他呼吁学界共建独立、透明的LLM基础设施。

亚马逊开源了验证器Verus，可为Rust代码提供数学证明，弥补类型系统仅能保证内存安全、无法保证结果正确的不足。规约以requires/ensures直接写入源码，普通编译器会将其擦除，不影响Cargo构建。Verus的自动求解器可秒级反馈，支持AI辅助证明，并能验证unsafe代码与并发锁的正确性。该工具已用于AWS Nitro隔离引擎核心组件，并被证书校验、Kubernetes控制器等开源项目采用。

陶哲轩宣布SAIR开放数学操作系统软启动，提供类似前沿AI的数学服务。平台托管DeepSeek V4.1 Flash、Kimi K3和GLM 5.3 Flash等开放模型，能力约落后前沿模型一年，但足以完成中等规模Lean形式化、总结数学论证等任务。平台强调团队账户，成员可互见提示词，适合协作。正招募伙伴微调数学专用模型，使用捐赠算力，向学术机构免费开放账户，欢迎反馈。

陶哲轩介绍，Jeremy Avigad、Kevin Buzzard等七位数学家在Buzzard博客发文《如何形式化全部数学》，讨论自动形式化整个数学文献的提议，并聚焦形式数学与常规数学在速度、规模与理解之间的权衡。

数学家Deanna Needell和Hayden Schaeffer发帖征集参与或促成AI辅助数学发现成果的数学家反馈，以记录人类洞见与AI协作的过程，了解前期研究、验证论证、联系文献等贡献。来信请寄mathematiciancontributions@gmail.com，内容保密，未经同意不会引用或署名。

美国数学学会2026年10月发布数学科学研究生教育报告，建议院系与前沿AI公司达成机构协议，将AI工具纳入科研流程并明确隐私与安全要求。评论者指出，企业隐私安全承诺难以强制执行，亟需建立类似区块链的研究进展记录机制。

傅里叶研究热传导的正弦余弦函数，现被用于大语言模型的位置编码。注意力机制不感知词序，需将位置转为数值表示。正弦余弦编码具有多频率、有界、平移一致的特点，模型经训练可借此理解语序；RoPE则将其用于旋转查询和键。

JetBrains公布2026–2027学年学生科技活动：免费青年数学、AI、编程俱乐部（10月31日前报名）；在塞浦路斯、波兰、塞尔维亚举办13–19岁编程杯；11月29日青年编程挑战赛分两组，优胜者可入选2027年3月塞浦路斯ACTS集训营，涵盖竞赛编程、软件工程和AI三个方向。

陶哲轩整理了近期关于数学与AI的博客和评论文章链接，供读者参考，并邀请大家在评论区补充更多相关链接。

陶哲轩提出“数学2.0”时代，认为AI使证明不再稀缺，冲击数学1.0评价体系。他警告AI能力不均与幸存者偏差，呼吁建立透明评估机制，重视理解、解释和知识整理，而非只奖励解题。他强调人类科学家的核心价值在于把关与理解，并指出AI时代读博仍可培养提出好问题等能力。

陶哲轩发布公开演讲“Math 2.0”幻灯片，回顾数学1.0的历史状态，分析当前AI过度强调自动解决未解问题带来的现状，并提出未来数学2.0愿景：用AI工具维系数学共同体，并维护数学理解在推动和校准数学现实应用中的作用。

OpenAI发布719份未公开前沿模型生成的数学手稿，含Lean形式化证明，引发透明度讨论。Mistral与Reflection AI推出开源权重模型，对标中国开源模型。OpenAI安全研究员David Robinson辞职，批评公司文化忽视安全。谷歌开放SynthID检测工具，OpenAI在欧盟为ChatGPT文本加水印。Anthropic发布Claude Haiku 5.5，价格大降90%。