把自己代入一位研究了二十年数学的学者：论文刚挂出来，质疑先到了——这么漂亮的证明，是不是AI生成的？你气得想笑，可环顾四周，发现自己真的拿不出一件能让所有人闭嘴的证据。
今天知乎热榜上就挂着这个问题：一位数学家如何证明自己没有使用AI做论文？乍看像个段子，但我把最近几个月的相关报道翻了一遍，发现这可能是今年学术圈最严肃的提问之一。
为什么这个问题没有标准答案
先看一个事实：“用AI做数学”已经走到了必须标注人机分工的程度。10月初中华网等媒体报道，Meta AI连破6大数学猜想，所有工作都是通过网页端meta.ai、靠自然语言提示词完成的；六篇论文经过独立双重审查，每篇都清晰标注了哪些部分由人类学者起草、哪些部分是AI独立生成。
当AI的产出开始比肩世界级成果，靠文本检测工具“自证清白”就彻底失效了——检测器查的是“像不像AI”，不是“是不是AI”。你写得越工整、越规范，反而越像机器。这就是这个问题的死结：它无法用一份检测报告来回答。
那怎么办？数学界其实已经给出了三种真实解法。
解法一：把成果交给机器核验
9月上旬，中科院数学与系统科学研究院联合Project Numina等团队，完成了三维挂谷猜想的形式化证明——约41.7万行Lean代码、907个源文件、7575条定理及引理声明，全部通过Lean 4内核的逐行机器核验。
这条路的聪明之处在于：它不争论“谁写的”，只让证明本身可被机器检查。形式化证明容不下任何逻辑跳步，AI写的还是人写的，过不了内核就是过不了。问题被悄悄置换了——从“证明你不是AI”，变成“证明结果是对的”。
但陶哲轩提醒过冷水的一面：机器验证的是形式陈述本身，而不是这个陈述和你原本想证的意图相符。8月，堪萨斯大学的J. L. Nielsen把OpenAI公开的37000行Lean 4代码逐行追踪，24小时内驳回了其“推翻Connes刚性猜想”的宣称——AI把每一句话都证对了，可证的已经不是原猜想。换句话说，机器核验也救不了最后一环：得有人为“命题对不对齐”负责。
解法二：拿出过程的痕迹
纽约大学阿布扎比分校的博士后Gajjala说过一句狠话：“在通过验证之前，一份漂亮的证明和垃圾没有区别。”他后来干脆离开学术界，转身加入刚拿到2700万美元种子轮的PramaanaLabs，专门做验证系统。
他这个转身，指向第二种解法：结果可以碰巧、可以伪造，但过程很难——草稿、版本记录、走不通的推导、深夜改掉的错误思路，这些“中间态”是事后最难补造的东西。陶哲轩给当下起了个词叫“证明的消化不良”：AI生成证明的速度远超人类审核的速度，证明正从稀缺品变成洪水。洪水时代，稀缺的不是答案，是可信的过程。
解法三：当场再推一遍
最古老，也仍然最硬的一招：当着质疑者的面，把论文里的关键步骤从头推一遍，讲清楚为什么走这条路而不是那条。理解无法外包——这是目前唯一一份AI替你交不出来的“证明”。
这跟你有什么关系
你大概率不写数学论文，但同款质疑正在逼近普通人：作业是不是AI写的？方案是不是AI生成的？连简历都可能被问一句“这段经历你能现场讲讲吗”。
三种解法照样成立。第一，别执着于自证“纯净”，那是证不出来的，方向本身就错了。第二，干活时留痕——文档开着版本记录，草稿别急着删，你的每一次迭代就是你的“Lean代码”。第三，对交出去的每一个关键结论，理解到能当场重推的程度；讲不明白的部分，要么弄懂，要么删掉。
AI时代真正的变化，不是“机器会写论文了”，而是人证明自己价值的方式变了：从“这是我写的”，变成“这是我懂的”。前者会越来越说不清，后者反而越来越值钱。
我平时就用spark1.cn的/ai-writer让AI出初稿，但版本记录和逐段改写都留在自己手里——初稿可以是机器的，定稿必须是你的。
本文素材综合自中华网、新智元、新浪科技、中科院数学与系统科学研究院官网等公开报道。
💬 评论