|
|
: a9 l" u- P9 N _
722 篇论文里，只有 162 篇经过了机器验证。。。。7 \3 g. O& G X6 P
- o% I+ Q% X* D( R- D u& y' T
把目录按论文日期拆开统计：9 月 22 日到 27 日那五天产出的五百多篇里，有 159 篇有形式化证明；而 10 月 3 日之后新增的一百四十多篇，一篇都没有。
# f, b# {! \" `1 m
8 G0 v( @' {' J( Q' T可能有人记得，2025 年 8 月 OpenAI 发过一个「十个数学进展」，当时也是 AI 产出的数学结果，也挂在 GitHub 上。。。。3 Y. `3 h5 z. y- \$ r
0 ]' V0 ^' p* e' J \
那 10 个结果，每一个都标着验证细节：证明文件、定理入口、未完成证明的占位符计数为零、允许使用的公理清单，全写明了，任何一个较真的数学家都可以照着清单自己复验。而这一次，162 篇有主结果形式化，一些条目自己标着「部分进展」「未复核」，还有 560 篇连机器验证都没有。。。。
; B2 J0 `* D, \9 u7 R% e6 X) Q3 Y V( L7 g; e" \8 J' S! |" p1 b
一年时间，产能翻了七十倍，验证比例从 100% 掉到了 22%。。。。
6 L5 G* \/ i6 B) b6 i% \( v+ b4 a- I! j- V
OpenAI 这次做的事情，本质是一样的：模型负责生成，Lean 负责盖章。模型可以天马行空，最终「算不算数」必须由一个确定性的裁判确认。
4 r+ f% b( L" T9 M+ j; m4 O0 E1 A' h4 N
数学能过形式化验证，所以数学成了 AI 科研的头号突破口；而医疗、法律、社会学这些「无法机器验证」的领域，AI 只能一直停在辅助诊断，替代不了签字权。。。。7 H( u3 s4 a7 x
7 n e! D5 b$ q( b
「先生成后验证」听起来很美，但验证跟不上时会发生什么？会发生这件事：AI 生产的未经证实的知识会大量堆在公共池子里，后来的人每引用一条，都得先判断它是不是那 78% 的一部分。。。& R3 f$ J3 Z' u
8 d' o* K% p' S下一次看到「AI 取得重大突破」的时候，先别激动，问一句：这个结果，谁来验证？
# u. {0 }* ]3 Q5 R# t# `8 q5 b4 F2 U# Q& z! B" T X% i
。。。 |
|
发表于 2026-9-2 23:35:32
楼主
