上海AI实验室助破三维Ghys猜想人类独家署名并公开验证账本

AI技术投降派

此次突破并非机器独立攻破数学猜想，其真正分量在于用公开账本确立了AI推演、人类负全责与形式化复查的技术边界。

AI-assisted summary of AI证出31年数学悬案？悬置多年的三维Ghys猜想 — original source. Check the original for full context.

Source published: 2026-10-16

Key ideas

上海人工智能实验室宣布借助书生S2内部版辅助证明了悬置31年的三维Ghys猜想，实际攻克的是复余维1情形（包含复三维），更一般的四维及更高维猜想仍处于开放状态。 (0:00)
19页学术论文唯一署名人由KTH博士后张洁松独立承担，明确声明作者已独立核验全部论证并负全责，AI仅作为提供推导草稿的协作者。 (2:46)
北大董彬与刘若川团队利用SHEAF引擎在5天内动用100个智能体生成55万行Lean形式化代码，实现了无sorry验证，但显式借入1969年Hsiang-Wall定理作为外部假设。 (4:01)
相较于OpenAI同期因批量发布722篇数学论文且迅速撤稿霍奇猜想等成果引发的争议，本项研究因完整公开分工账本与边界条件而展现出更高科研信度。 (5:06)

Detailed notes

## Background 该视频由B站UP主“AI技术投降派”于2026年10月16日发布。视频围绕上海人工智能实验室官宣的“许地生团队借助书生S2人机协同证明悬置31年的三维Ghys猜想”展开，重点剖析大多数报道忽略的论文声明“作者独立核验并负全责”，详细拆解AI、人类学者与形式化验证机器各自承担的工作与边界。

## TL;DR 视频深入剖析了复三维Ghys猜想被攻克的全过程与真实边界：该工作严格证明了复余维1（含复三维）的情形，而更高维仍处于开放状态。在整个研究链路中，书生S2内部版作为辅助工具扩展了推演思路，产出千页推导报告；论文唯一署名作者张洁松独立核验了全部数学论证并承担全责；随后北大团队通过SHEAF引擎在5天内生成约55万行Lean代码完成机器形式化复查，同时明确标明外借了1969年的Hsiang-Wall定理作为显式假设。视频对照OpenAI大量发布数学论文又撤稿的乱象，指出这套“AI出思路、人守验证、机器查推理”的透明账本才是推动当代数学研究的最宝贵范式。

## Atmosphere & style 全片呈现出极度冷静、严谨且去魅的硬核科普质感。UP主语气克制清醒，不跟风宣扬“AI攻克猜想”的狂欢式口号，而是像审计员拆解账目一样抽丝剥茧，将数学边界、责任归属与机器验证的红字明码标价。叙事节奏紧凑从容，在宏大历史预言与微观代码细节的穿插对照中，流露出对严谨科学伦理的敬意，给观众带来一种穿透宣发迷雾、看清前沿科研真实运作方式的通透与踏实感。

## Bulletin - [00:00](https://www.bilibili.com/video/BV1TSJD66Eg7?t=0s) 上海人工智能实验室宣布借助书生S2内部版辅助证明了悬置31年的三维Ghys猜想，实际攻克的是复余维1情形（包含复三维），更一般的四维及更高维猜想仍处于开放状态。 - [02:46](https://www.bilibili.com/video/BV1TSJD66Eg7?t=166s) 19页学术论文唯一署名人由KTH博士后张洁松独立承担，明确声明作者已独立核验全部论证并负全责，AI仅作为提供推导草稿的协作者。 - [04:01](https://www.bilibili.com/video/BV1TSJD66Eg7?t=241s) 北大董彬与刘若川团队利用SHEAF引擎在5天内动用100个智能体生成55万行Lean形式化代码，实现了无sorry验证，但显式借入1969年Hsiang-Wall定理作为外部假设。 - [05:06](https://www.bilibili.com/video/BV1TSJD66Eg7?t=306s) 相较于OpenAI同期因批量发布722篇数学论文且迅速撤稿霍奇猜想等成果引发的争议，本项研究因完整公开分工账本与边界条件而展现出更高科研信度。

## Key takeaways - [00:39](https://www.bilibili.com/video/BV1TSJD66Eg7?t=39s) Ghys猜想由法国数学家艾蒂安·吉斯于1995年提出，探讨复动力系统中极端的混沌拉扯与苛刻的全纯光滑性叠加时所产生的几何刚性。 - [01:12](https://www.bilibili.com/video/BV1TSJD66Eg7?t=72s) 复分析中的全纯具有牵一发而动全身的全局约束力，吉斯猜想全纯混沌系统的自由度将被压为零，使其形态被锁定在环面等经典代数变换上。 - [01:53](https://www.bilibili.com/video/BV1TSJD66Eg7?t=113s) 猜想中的三维指复三维（对应实空间六维），而非物理学中洛伦兹吸引子所属的实三维系统。 - [02:13](https://www.bilibili.com/video/BV1TSJD66Eg7?t=133s) 本次证明的核心突破在于复余维1情形，因为复三维的两个伸缩方向相加为3且必有一个为1，故三维情况被完全包含并解决。 - [02:38](https://www.bilibili.com/video/BV1TSJD66Eg7?t=158s) 数学上复四维及以上维度已存在非环面反例，更一般的完全Ghys猜想依然向学界敞开。 - [03:16](https://www.bilibili.com/video/BV1TSJD66Eg7?t=196s) 书生S2在推导过程中经历7批演化，将问题图从15个节点扩展至389个节点，累计输出千页草稿，但方向把控仍由人类数学家完成。 - [03:46](https://www.bilibili.com/video/BV1TSJD66Eg7?t=226s) 论文由张洁松独立署名，表明人机协同研究中最终的学术把关和法律伦理责任依旧落在人类研究者身上。 - [04:15](https://www.bilibili.com/video/BV1TSJD66Eg7?t=255s) 北大团队动用SHEAF引擎完成Lean交互式定理证明，峰值使用100个智能体、生成55万行代码，未自设公理且无sorry空洞。 - [04:38](https://www.bilibili.com/video/BV1TSJD66Eg7?t=278s) 机器复查显式借用了1969年的Hsiang-Wall定理，凸显形式化验证只能保证推导链无漏洞，前提假定与文本转译忠实性仍需人类负责。 - [05:13](https://www.bilibili.com/video/BV1TSJD66Eg7?t=313s) OpenAI此前一次性发布722篇AI论文并在24小时内因严重漏洞撤稿3篇，反衬出明确界定模型辅助边界与公开账本的重要性。 - [05:32](https://www.bilibili.com/video/BV1TSJD66Eg7?t=332s) 艾蒂安·吉斯曾在2023年预言大语言模型既是数学家的想象同事，也可能制造出色的科学赝品，本次证明展现了人机协同的现实解法。 - [06:03](https://www.bilibili.com/video/BV1TSJD66Eg7?t=363s) 此项成果的真正价值不仅在于解决猜想，更在于确立了“AI出思路、人守验证、机器查推理”的透明化科研范式。

## Detailed walkthrough ### [00:00](https://www.bilibili.com/video/BV1TSJD66Eg7?t=0s) 混沌加全纯等于刚性：悬置31年的三维Ghys猜想

10月15日，上海人工智能实验室官宣：许地生团队借助书生S2模型，人机协同证明了悬置31年的三维Ghys猜想。然而在铺天盖地的报道中，许多人忽略了论文中最关键的一行声明：“作者独立核验了全部论证，并对稿件负全责。”要厘清这个成果的真正分量，必须先把账本拆开看：AI到底干了什么、人守住了哪一关、机器又查到了哪条线。

这一猜想源于1995年法国数学家艾蒂安·吉斯（Étienne Ghys）提出的深刻问题：在复数世界里，最混乱的动力系统究竟能乱到什么程度？其原型可追溯至经典的阿诺索夫（Anosov）系统。设想一张格子纸糊成的环面，上面施加一个变换，每进行一次操作，就将一个方向拉长、另一个方向压扁；随着变换不断反复，图形被彻底撕裂，系统轨道对初始条件产生极端敏感的依赖——这便是教科书级别的混沌。

吉斯在此基础上探寻复数版本：如果这一整套拉扯撕扯的动作是“全纯”的（即复分析意义上的无限次光滑），动力系统会发生什么变化？全纯是一个远比普通实数光滑苛刻得多的约束条件，局部极其微小的信息就能直接决定全局性态，“牵一发而动全身”。吉斯敏锐地猜想：混沌与全纯这两个最强的约束叠加在一起，会硬生生将系统的自由度压到零；这样的系统必然长得像典型的代数变换，绝不可能存在第二种形状。这就是数学中所说的“刚性”（Rigidity）——越是允许它呈现混沌的复杂性，内在规律反而越把它死死钉在最简单的形态上。吉斯在1995年亲自解决了复二维的情形，但将更一般的维数问题留给了后人，这一悬案一悬便是31年。

[01:53](https://www.bilibili.com/video/BV1TSJD66Eg7?t=113s) 复三维等于实六维：证明边界与高维开放性

理解这项证明首先需要厘清“三维”的概念。这里的“三维”是指复三维，换算到实空间等价于实六维，与物理学中著名的洛伦兹吸引子那种实三维混沌完全不是一回事。论文实际证明的是“复余维为1”的情形。通俗而言，在系统拉长和压扁的两个方向中，只要其中有一个方向是复一维的，结论便成立；而复三维天然落在该范畴内，因为拉长和压扁方向的维数都必须非零，相加为3时必然有一方是一维。因此，新闻报道宣传“三维Ghys猜想被证明”，其科学口径是准确的。

然而，更一般的完整猜想目前依然处于开放状态。从复四维开始，数学上存在不长得像环面的反例，高维世界必须允许其他形状存在，那扇通往完全解答的大门至今仍未完全推开。

```mermaid flowchart TD accTitle: Ghys猜想各维数解决状态 accDescr: 展示从复二维、复三维到复四维及以上Ghys猜想的解决进展与现状

subgraph Solved ["已解决情形"] D2["复二维 (Étienne Ghys, 1995)"] D3["复三维 / 复余维1 (张洁松, 2026借助书生S2)"] end

subgraph Open ["开放情形"] D4["复四维及更高维 (存在非环面反例，猜想仍开放)"] end

D2 -->|"推进至余维1"| D3 D3 -.->|"高维大门仍关着"| D4 ```

[02:46](https://www.bilibili.com/video/BV1TSJD66Eg7?t=166s) 人机协同：从15到389个节点的问题图，署名只有张洁松

整篇论文共19页，而论文的署名人从始至终只有一位：张洁松。他是许地生指导出来的博士生，目前正在瑞典皇家理工学院（KTH）从事博士后研究。许地生本人过去曾与菲尔兹奖得主阿图尔·阿维拉（Artur Avila）深入合作探索过该猜想的三维情形，这次正是他将这一难题带入了上海人工智能实验室的访问研究中。

在这项工作中，书生S2扮演了强大的“陪跑”角色。其前代科学模型书生S1在2025年首次中国数学奥林匹克AI测试中斩获102分的高分（当时金牌线仅为78分），而S2作为继承者刚于9月开源发布，但在证明中投入使用的是未公开的实验室内部版本。在官方披露的人机协同机制中： - S2在首轮推理中就输出了长达400页的推导报告； - 历经先后7批接续推演，推理“问题图”从初始的15个核心节点一路繁衍扩展至389个节点，累计输出草稿达千页规模； - 这一赛道的门槛极高，北京大学谢君毅教授也曾尝试使用GPT-6挑战该题，但未获成功，证明并非任何模型都能介入这种高精尖命题。

人与机器的分工泾渭分明：判断问题突破口、校准推演方向、将零散论证最终组装起来的，是许地生和张洁松；而承担最重学术责任的唯有张洁松一人，每一个推理步骤均由他亲自核验，全部学术责任也完全由他一人担起。

[04:01](https://www.bilibili.com/video/BV1TSJD66Eg7?t=241s) 机器复查：5天55万行Lean代码，以及账本里的红字假设

在人类完成推导核验后，研究引入了第三道严密的工序——机器形式化复查。北京大学董彬与刘若川团队利用自研的SHEAF引擎，将论文中的四个主定理以及所援引的吉斯1995年经典结果，完整翻译为Lean交互式定理证明语言，交由计算机进行逐行检验。

这项形式化验证耗时5天，峰值时期动用了100个智能体并行协同作业，最终产出约55万行Lean代码。整个代码仓库对外公开，没有留下任何未完成证明的“sorry”空洞，也没有随意自设公理。但在这一严谨的机器账本中，清清楚楚写着一行“红字”： - 项目形式化过程将1969年的一项经典定理（Hsiang-Wall定理）作为显式假设直接引入，并未在项目内部对其进行从头到尾的重证。

这在现代数学形式化工程中是通行的标准做法——将学界公认无误的历史结果当作显式输入，集中有限算力去攻坚全新的核心推理链条。但这也划定了机器验证的明确边界：从既定假设到最终结论的每一步逻辑推理，机器保证绝对严密无漏洞；然而引入的外部假设本身是否成立、自然语言论文向Lean代码的翻译是否绝对忠实于原作，责任依然全在人类学者身上。一周前，著名数学家托马斯·黑尔斯（Thomas Hales）在陶哲轩的博客上公开发表的讨论，提醒的正是这一关键边界。

```mermaid flowchart LR accTitle: 三道工序验证流 accDescr: 展示从AI提供思路、人类数学家核验到机器形式化复查的全流程

subgraph Step1 ["第一道工序：AI陪跑"] A["书生S2内部版 7批推演 / 1000页输出 问题图：15 → 389节点"] end

subgraph Step2 ["第二道工序：人类掌舵"] B["许地生 & 张洁松 确定突破口、校准方向"] C["张洁松（独立署名） 独立核验全部论证并负全责"] B --> C end

subgraph Step3 ["第三道工序：机器形式化"] D["北大董彬/刘若川团队 SHEAF引擎 + Lean形式化"] E["5天 / 100个智能体 / 55万行代码 无sorry / 无自设公理 红字：外借1969年定理为假设"] D --> E end

A --> B C --> D ```

[05:06](https://www.bilibili.com/video/BV1TSJD66Eg7?t=306s) 722篇撤稿对照与吉斯的预言：一本公开的账本最值钱

将视野拉远，就在这项成果公布的两周前，OpenAI曾一口气公开了722篇由AI生成的数学论文，结果在短短24小时之内就紧急撤回了3篇，且涉事题目竟然包括霍奇猜想（Hodge conjecture）这类千禧年大奖难题级别的命题。对比这种混乱的“大干快上”，本次证明展现出的最大价值恰恰是“那本清晰公开的账本”：究竟谁出了思路、谁负责核验、机器复查到了哪条边界、借用了哪些前置假设，全都白纸黑字对外公开、有迹可循。

这其中充满了数学史的戏剧性色彩。早在2023年，埃蒂安·吉斯本人就曾撰文谈论过大语言模型，他写道：ChatGPT就像是数学家的“想象同事”，是一个读遍了一切、连所有错误也一并读过的伙伴；但他当时也同时发出警告，认为这也是一种“能制造出色科学赝品的智能”。三年之后，吉斯当年留下的猜想，恰恰以一种他曾预言过的人机协同方式向前迈出了一大步：“AI出思路，人守验证，机器查推理。”截至目前，吉斯本人尚未对此公开表态。

剖析这一事件，最终沉淀下来的结论其实只有三句话： 1. **证明是真的**：但适用范围是复余维为1（复三维自然包含在内），高维情形依然处于开放状态； 2. **AI的角色是真的**：但它仅负责陪跑推演，论文的独家署名与最终责任全由人类数学家承担； 3. **机器验证是真的**：但信任的技术边界被诚实地标了价、写在账本上。

正如视频所总结的那样：“一本公开的账本，比一句‘AI攻克猜想’值钱得多。”

## Notable quotes > [05:06](https://www.bilibili.com/video/BV1TSJD66Eg7?t=306s) 一本公开的账本，比一句‘AI攻克猜想’值钱得多。 — AI技术投降派

> [05:06](https://www.bilibili.com/video/BV1TSJD66Eg7?t=306s) AI出思路，人守验证，机器查推理。 — AI技术投降派

## Mentioned 艾蒂安·吉斯 (Étienne Ghys), 许地生, 张洁松, 阿图尔·阿维拉 (Artur Avila), 董彬, 刘若川, 谢君毅, 托马斯·黑尔斯 (Thomas Hales), 陶哲轩, 上海人工智能实验室, 北京大学, 瑞典皇家理工学院 (KTH), OpenAI, 书生S2, 书生S1, SHEAF引擎, Lean, GPT-6, Ghys猜想, Hsiang-Wall定理, 霍奇猜想, 阿诺索夫系统 (Anosov)

## Video description 10月15日，上海人工智能实验室官宣：许地生团队借助书生S2，人机协同证明了悬置31年的三维Ghys猜想。转报道铺天盖地，但论文里有一句话被大多数人漏掉了："作者已独立核验全部数学论证，并对稿件负全责。"这期把这本账拆开看：AI干了什么，人守住了哪一关，机器又查到了哪条线。

00:05 开场：被埋掉的一句话 00:39 猜想是什么：混沌+全纯=刚性 01:53 证明了什么：复三维=实六维，高维仍开放 02:46 人机协同：问题图15→389节点，署名的只有张洁松 04:01 机器复查：5天55万行Lean，账本红字明码标价 05:06 大图景：对照OpenAI 722篇撤稿，吉斯本人的预言 06:03 结论：三句话

三个容易混淆的点先说清。这次证明的是复余维1情形（复三维在内），完整猜想还开放。论文唯一署名人是张洁松（KTH博士后、许地生的博士生），许地生是导师和组织者。S2用的是内部版，多轮对话辅助思路，全部论证由作者独立核验。第三道工序是北大董彬、刘若川团队用SHEAF引擎做的Lean形式化：5天、峰值100个智能体、约55万行代码、无sorry。但账本里有一行红字：借入1969年的Hsiang-Wall定理当显式假设，没有在项目内重证。机器查的是推理链，假设与翻译忠实性仍是人的责任。

AI出思路，人守验证，机器查推理。一本公开的账本，比一句"AI攻克猜想"值钱得多。

论文：arxiv.org/abs/2609.37695 形式化代码：github.com/frenzymath/HolomorphicAnosov

[Source](https://www.bilibili.com/video/BV1TSJD66Eg7)

中文简报

上海AI实验室助破三维Ghys猜想人类独家署名并公开验证账本此次突破并非机器独立攻破数学猜想，其真正分量在于用公开账本确立了AI推演、人类负全责与形式化复查的技术边界。视频深入剖析了复三维Ghys猜想被攻克的全过程与真实边界：该工作严格证明了复余维1（含复三维）的情形，而更高维仍处于开放状态。在整个研究链路中，书生S2内部版作为辅助工具扩展了推演思路，产出千页推导报告；论文唯一署名作者张洁松独立核验了全部数学论证并承担全责；随后北大团队通过SHEAF引擎在5天内生成约55万行Lean代码完成机器形式化复查，同时明确标明外借了1969年的Hsiang-Wall定理作为显式假设。视频对照OpenAI大量发布数学论文又撤稿的乱象，指出这套“AI出思路、人守验证、机器查推理”的透明账本才是推动当代数学研究的最宝贵范式。上海人工智能实验室宣布借助书生S2内部版辅助证明了悬置31年的三维Ghys猜想，实际攻克的是复余维1情形（包含复三维），更一般的四维及更高维猜想仍处于开放状态。 (0:00) 19页学术论文唯一署名人由KTH博士后张洁松独立承担，明确声明作者已独立核验全部论证并负全责，AI仅作为提供推导草稿的协作者。 (2:46) 北大董彬与刘若川团队利用SHEAF引擎在5天内动用100个智能体生成55万行Lean形式化代码，实现了无sorry验证，但显式借入1969年Hsiang-Wall定理作为外部假设。 (4:01) 相较于OpenAI同期因批量发布722篇数学论文且迅速撤稿霍奇猜想等成果引发的争议，本项研究因完整公开分工账本与边界条件而展现出更高科研信度。 (5:06)

Reading summary

上海人工智能实验室团队借助书生S2模型人机协同证明了悬置31年的三维Ghys猜想，但该成果的科学价值不仅在于推进了复余维为1的刚性问题，更在于建立了一套责任明晰、边界公开的人机协同与形式化验证范式。混沌与全纯叠加的动力系统刚性 (0:00) 该猜想由法国数学家艾蒂安·吉斯于1995年提出，源于经典阿诺索夫系统。系统在复数世界中若同时满足混沌撕裂与“全纯”（无限次光滑）两个苛刻约束，其自由度会被压缩至零，系统形态必然被钉死在最简单的典型代数变换上，即表现出数学上的“刚性”。吉斯在1995年解决了复二维情形，更一般维度的难题则悬置了31年。三维成立与更高维度的开放边界 (1:53) 本项研究所证明的“三维”是指复三维（等价于实六维），并非物理学中的实三维洛伦兹吸引子。论文实际证明的范围是“复余维为1”的情形，即拉长或压扁方向中至少有一个是复一维，复三维因维数相加为3而必然包含其中，因此新闻口径准确。然而，该猜想对于复四维及更高维度仍未推开大门，高维世界中已证实存在非环面的反例，完整猜想依旧处于开放状态。千页草稿推演与人类学者的学术全责 (2:46) 19页的论文仅由许地生的博士生、瑞典皇家理工学院博士后张洁松一人独立署名。书生S2未公开内部版扮演了“陪跑”角色，在首轮输出400页报告，历经7批推演将推理问题图从15个节点扩展到389个节点，生成上千页草稿。尽管北京大学谢君毅此前尝试GPT-6未果，显示出该赛道的高门槛，但整项研究中判断突破口、校准方向与组装论证的均是许地生与张洁松，且由张洁松独立核验全部论证并承担全部学术责任。 55万行代码核验与外借公理的红线 (4:01) 为确保推理无误，北京大学董彬与刘若川团队利用SHEAF引擎，历时5天、动用峰值100个智能体并行作业，将论文的4个主定理及吉斯1995年结果翻译为约55万行Lean代码。该形式化验证没有使用“sorry”空洞或自设公理，但明确标注了一项“红字”假设：直接引入了1969年的Hsiang-Wall定理而未在项目内从头重证。正如托马斯·黑尔斯在陶哲轩博客讨论中所指出的，机器能保证从前置假设到结论的链条严密，但假设本身的正确性与自然语言转译的忠实度仍由人类学者负责。透明账本对冲生成式论文乱象 (5:06) 在成果公布前两周，OpenAI曾公开发布722篇AI生成的数学论文，却在24小时内紧急撤回3篇涉霍奇猜想等难题的稿件。与之对比，本项工作的核心价值在于提供了一本公开透明的账本：谁出思路、谁担责任、机器复查的边界以及外借的前提假设均清晰可见。这印证了吉斯在2023年关于AI是“连错误也一并读过的想象同事”并可能制造“出色科学赝品”的论述，实现了“AI出思路，人守验证，机器查推理”的协作机制。本项成果证明了复余维1情形下的Ghys猜想，AI提供了大规模推演支持，机器完成了55万行代码的形式化检验，但高维猜想仍未解决，且整个链条的信任边界建立在对历史定理的显式假设与人类数学家独立承担的学术责任之上。

Source quotes

[5:06] AI技术投降派: 一本公开的账本，比一句‘AI攻克猜想’值钱得多。 [5:06] AI技术投降派: AI出思路，人守验证，机器查推理。

Original transcript

[0:00] AI又攻克数学猜想了10月15号,上海人工智能实验室官宣。许蒂生团队借助书生S2模型,人机协同证明了玄至31年的三维吉斯猜想,但同一波新闻里,有一句话被大多数转报道埋掉了。论文里写着,作者独立核验了全部论证,并对稿件负全责。这期我们拆开这本帐AI干了什么人守住了哪一关机器又查到了哪条线先说这个猜想本身,1995年,法国数学家埃蒂安吉斯提出了一个问题,在复数世界里,最混乱的动力系统能乱到什么程度?这要从阿诺索夫系统说起,想象一张格子纸糊成的环面,上面有个变幻,每做一次,就把一个方向拉长,另一个方向压扁,反复做下去,图形被撕的粉碎。轨道对初始条件极端敏感这是教科书籍的混沌吉斯问的是复数版如果这套撕扯动作是全唇的也就是复分析意义上的光滑会怎么样全唇是比光滑强得多的约束局部一点点信息就能决定全局迁移范而动全身吉斯猜想混沌加全唇两个最强的约束叠在一起会把自由度压到零这样的系统必然长得像变幻没有第二种形状这就是数学里说的刚性越是允许他乱规律越把他盯死在最简单的样子上他自己解决了负二维的情形,把一般问题留给了后来人,一选就是三十一年。这次的论文证到了哪一步?先澄清三维这个词它是负三维等于十六维跟洛伦兹西银子那种十三维混沌不是一回事论文证明的是负于为为一的情形通俗说拉长和压扁两个方向里有一个是负一为的负三为自动落在这个范围内因为两个方向都得飞零必有一个是一为所以新闻说三维吉斯猜想被证明口径是准确的。但完整的一般猜想还没有证明从负四为起存在不长得像环面的反例高维世界必须允许别的形状那扇门还关着论文十九页署名只有一个人张杰松许帝生代的博士生现在瑞典皇家里工作博士后那书生S2扮演什么角色先看家底书生S1在2025年首次中国数学奥林匹克AI测试里拿了102分金牌线是78S2是他的科学模型继任者今年9月刚发布开源但这次论文用的是内部版任务是陪跑研究官方披露的作业方式里第一轮推理就产出400页推导报告先后7批接续推演问题图从15个节点涨到389个总输出约千页北大教授谢君毅的注脚很说明问题他也用GPT6试过这道题没做出来不是随便一个模型都能进这个赛道人的位置同样清楚徐笛生曾与菲尔兹奖得主阿维拉合作研究这个猜想的三维情形他把问题带进了上海实验室的访问研究判断突破口校准方向再把证明组装起来是许地生和张杰松两个人而最后在论文上署名的只有张杰松一个人,每一部论证他亲自合言。全部责任也由他承担论证何彦丸还有第三道工序机器复查北大董斌刘若川团队用自研的Shade AF引擎把论文四个主定里连同用到的集思1995年结果翻译成另语言让计算机逐行检验,五天时间,峰值100个智能体并行,产出约55万行代码。仓库公开没有空洞也没有自设公理但账本里有一行红字形式化介入了一个1969年的经典定理当假设没有在项目里重症这在形式化里是标准做法,把公认的旧结果当显示输入,把验证火力集中在新的推理上。但要想明白机器查的是什么?从假设到结论的每一步推理,机器保证无漏洞。至于假设本身,还有翻译是否忠实于原论文,仍然是人的责任。 [5:00] 一周前,数学家黑尔斯在陶哲轩的博客上提醒的正是这一点。把镜头拉远就在两周前,OpenAI一页公开722篇AI生成的数学论文,24小时内撤回三篇,涉事的还是获奇猜想这个级别。相比之下这次多出来的东西是那本账谁的思路,谁的荷燕?机器查到哪条线见了哪个假设?全部公开可查最有戏剧性的是集思本人2023年,他写过一篇文章,说ChatGPT是数学家的想象同事,一个独遍一切,连错误也读过的伙伴,但他同时警告这是能制造出色科学赚品的智能。三年后,他的猜想以一种他预言过的方式被推进AI出思路,人手验证,机器查推理。截止目前,集司本人没有公开表态。所以这期的结论有三句,证明是真的,范围是负于维为一,负三维在内。高维仍开放AI的角色是真的但他只负责陪跑署名和责任都在人机器验证是真的但信任的边界被诚实地标了架一本公开的账本比一句AI功课猜想之前的多论文和形式化代码都放在简介里下期再见

上海AI实验室助破三维Ghys猜想 人类独家署名并公开验证账本