AI 半小时证出人类一年没做出的数学定理
一个被卡住的 L^p 问题，AI 用半小时给出五页证明，把 60 页的论文压缩成核心引理，还顺手把连续密度的门槛从 588 推到 9。
核心论点 · 点时间戳可跳到原声
AI 第一次给出了好想法
讲者说这是他第一次遇到模型在一个他长期研究的问题上「really had a good idea」，而且这个想法导向了「very elegant efficient progress」。注意他的措辞：不是 AI 帮他算，是 AI 给出了他没想到的证明思路。他把这个结果归功于 Astra，并说这是上周才做出来的。
— Constantin Kogler关键定理：绝对连续自动带 L^p
核心定理是：如果自相似测度 μ 绝对连续，那它的密度自动落在某个 L^p 里，p 大于 1。真正让讲者兴奋的不是这个事实本身，而是 p 是定量的——p 可以用 μ 给小球的质量来显式表达。正因为 p 定量，才能把研究显式绝对连续性的方法搬过来，去构造显式的 L^p 例子，再进一步拿到连续密度。
— Constantin Koglerp 不可能做成一致的
讲者特别提醒：p 永远不能做成 uniform。对任意维数 d 和任意 p 大于 1，都存在某个自相似测度落在 L^1 但不落在 L^p。所以这个定量结果不能理解成「所有绝对连续的自相似测度都有一致的 L^p 可积性」——它是个逐例的、依赖质量分布的界。
— Constantin Kogler把 λ 拆成奇偶两部分
证明连续密度的技巧：把 Bernoulli 卷积的随机级数按奇偶项拆开，奇数部分提出一个 λ 后，剩下的正好是偶数部分。于是 μ_λ 等于 μ_{λ²} 与自身的卷积。如果 λ² 落在 Solomyak 证明的 L^2 几乎必然成立的范围里，两个 L^2 函数的卷积是连续的，就得到 μ_λ 有连续密度。这是从 L^2 结果推出连续性的桥梁。
— Constantin Kogler60 页论文被压成 5 页
讲者说核心想法其实是他和合作者已有的，但 AI 在使用这个想法时「extremely elegant and efficient」。Varju 的论文 60 页，他自己的论文也很长，AI 把从某个结果推到另一个结果的过程压缩到 5 页，而且「maybe a bit of a weakening」之后，再给 5 页就能拿到更强的结论。他强调这不是 AI 替他想了核心 idea，是 AI 把已知工具以他「could have never」的方式组合起来。
— Constantin Kogler半小时跑完，50 小时形式化
有人问运行时间，讲者说「not long, maybe half an hour」。之后整个结果在 Lean 里形式化，大约花了 50 小时。他还提到有 goal command 之类的技巧可以让模型「really try hard」。对比是：他自己可能要做一年，而且「if you sent me this paper to referee, I would like who is this person?」
— Constantin Kogler连续密度的门槛从 588 推到 9
对 λ = 1 - 1/n 的情形，AI 证明 μ_λ 在 n 大于 588 时连续——讲者说这还不是他 push 常数的结果，「if I push the constant, I could easily push the constant more」。更狠的是另一个结果：n 大于 9 时绝对连续，讲者说「I could not dare think I could prove」，他自己 push 了两个半小时才到 9，而理想目标是 3。
— Constantin Kogler关键引理来自冷门论文
证明的核心是一个来自几何测度论的引理：对 L^1 正函数 f，如果小球里集合的质量小，且 f 在该集合上的积分也小，就能推出 f 落在某个显式的 L^p 里，p 由 C、ε、A 显式给出。讲者说这个引理「not too difficult to prove」，大约一页，但「extremely difficult to find because it's not a very well-known fact」——它是从一些随机论文里挖出来的。
— Constantin Kogler原话 · 已逐字校验
it was the first time for me where where the models really had a good idea. So they had a good idea on a problem I worked long about that le led to progress like very elegant efficient progress I was very happy with.
这是我第一次遇到模型真的有好想法。它们在一个我研究了很久的问题上有了好想法，带来了非常优雅、高效的进展，我非常满意。
Constantin Kogler0:18
the AI was extremely elegant and efficient in using it so var's paper is 60 pages okay my paper is k does many things but it's also it's also a long paper the AI reduced to five pages
AI 在使用这个想法时极其优雅高效。Varju 的论文有 60 页，我的论文也做很多事、也很长，AI 把它压缩到了 5 页。
Constantin Kogler34:17
it just used these things that I knew. It used the tools I used too, but it just combined it in a way I could have never.
它用的就是我知道的那些东西，用的也是我用过的工具，但它以一种我永远不可能做到的方式把它们组合了起来。
Constantin Kogler37:19
if you sent me this paper to referee, I would like who is this person? I mean, this is like it was it's a if this is the smartest person in the world, I would say fine. But uh but I've never seen anything like this.
如果你把这篇论文发给我审稿，我会想：这人是谁？如果这是世界上最聪明的人写的，那行。但我从没见过这样的东西。
Constantin Kogler37:19
That's me not trying hard. That's not me. This is not me trying to run the I can push the constant more, but it's just it's just the eye chilling and p pushing.
这不是我在使劲。这不是我。我还能把常数推得更好，但这只是 AI 在轻松地推。
Constantin Kogler39:21
if you're an analytic number theorist if you want to calculate something these things are unbeliev like uncomparable to us in calculations.
如果你是解析数论学家，想算点什么东西，这些模型在计算上和我们完全不可同日而语。
Constantin Kogler41:22
it's extremely difficult to find because it's not a very well-known fact. It's some random fact from wherever.
它极难找到，因为这不是一个广为人知的事实。它是从某个地方冒出来的冷门事实。
Constantin Kogler44:23
数字与实体
| AI 证明运行时间 | 约半小时 | 36:18 |
| Lean 形式化耗时 | 约 50 小时 | 36:18 |
| Varju 论文页数 | 60 页 | 34:17 |
| AI 压缩后证明页数 | 5 页 | 34:17 |
| 连续密度门槛 n | 大于 588 | 39:21 |
| 绝对连续门槛 n | 大于 9 | 41:22 |
| 理想目标门槛 n | 3 | 41:22 |
| 讲者 push 常数耗时 | 约两个半小时 | 41:22 |
术语
- self-similar measure自相似测度
- 由有限个压缩相似映射生成的、满足自相似方程的概率测度，通常是分形对象。
- Bernoulli convolution伯努利卷积
- 随机级数 Σ ±λ^n 的分布，λ 在 0 到 1 之间，是研究绝对连续性的经典模型。
- absolutely continuous绝对连续
- 测度可以写成某个 L^1 函数对勒贝格测度的积分，即存在密度函数。
- L^p densityL^p 密度
- 密度函数落在 L^p 空间里，p 越大要求密度越「不集中」。
- LeanLean
- 交互式定理证明器，用于把数学证明形式化到机器可验证的程度。
收听指南
对 AI 在纯数学中实际能力感兴趣的数学研究者、理论计算机科学家，以及想知道「AI 做证明」具体长什么样的工程师。
前半段自相似测度和伯努利卷积的基础定义可以快进，直接听 33 分钟后的 AI 部分。