免责声明：我曾给予Grok 4.20内部测试版的早期访问权限。 它为我和我的学生N. Alpay一起研究的一个问题找到了一个新的Bellman函数。 这个问题归结为在两个约束下识别逐点最大函数U(p,q)并理解U(p,0)的行为。 在我们的论文中，我们证明了U(p,0)\geq I(p)，其中I(p)是高斯等周剖面，I(p) ~ p\sqrt{log(1/p)}当p ~ 0时。 大约5分钟后，Grok 4.20产生了一个显式公式U(p,q) = E \sqrt{q^2+\tau}，其中\tau是从p开始的布朗运动从(0,1)的退出时间。这导致U(p,0)=E\sqrt{\tau} ~ p log(1/p)在p ~ 0时，这是对对数因子的平方根改进。 这个结果有什么重要性？它不会告诉你如何在明天改变世界。相反，它为理解布尔函数的导数的随机类比的平均值发生了什么提供了一个小步骤：它们可以有多小？ 更准确地说，这为应用于集合A \subset [0,1]的指示函数1_A的二元平方函数的L1范数提供了一个严格的下界。 在我之前关于Takagi函数的推文中，我们看到||S_1(1_A)||_1的严格下界奇迹般地与|A|的Takagi函数重合，这让我感到惊讶的是，它与黎曼假设有关。在这里，我们获得了||S_2(1_A)||_1的严格下界，由E \sqrt{\tau}给出，其中布朗运动从|A|开始。这个函数属于等周剖面类型的家族，但与分形Takagi函数不同，它是光滑的，并且与高斯等周剖面不重合。 最后，在谐波分析中，已知平方函数在L^1中是不有界的。这里的问题更多是出于好奇：当在布尔函数1_A上测试时，它究竟是如何爆炸的。之前，已知的最佳下界是|A|(1-|A|)（Burkholder—Davis—Gandy）。在我们的论文中，我们得到了|A|(1-|A|)\sqrt{log(1/(|A|(1-|A|)))}。这个新的Grok的Bellman函数给出了|A|(1-|A|) \log(1/(|A|(1-|A|)))，这个界限实际上是严格的。

如果你继续用 LLM 测试 Erdős 问题，很可能最终会解决其中一个未解决的问题。专家们并没有这样做（出于显而易见的原因）。非专家们假设专家们在这样做。其实他们并没有。

安装Aristotle。获取API密钥。从终端运行它。选择数学中的任何开放问题，并以自然语言输入到aristotle中！经过几个小时，它要么会生成完整的正式lean证明，要么可能会失败。👏