AI不仅解决了数学家Erdős的百年猜想#728，更在Lean中完成了完整的形式化证明。这一事件的意义远超问题本身，它展示了AI在复杂数学推理中的惊人能力。通过拆解其证明过程，可以窥见AI是如何进行创造性思考和结构化论证的。
智能速览
ChatGPT 5.2与工具Aristotle合作，成功解决了数学开放问题Erdős #728。
该问题难度约为有天赋的研究生水平，属于适合当前AI工具攻克的“低垂果实”。
证明的核心是将整除性问题转化为p-adic不等式，并利用库默尔定理计算进位次数。
AI通过概率论方法，证明在绝大多数情况下，进位次数的下界足以满足整除条件。
整个证明过程被成功形式化为Lean代码，确保了逻辑的严密性和可验证性。
精华内容
这个证明不是魔法，而是融合了数论、概率和形式化验证的结构化论证，其核心思想精妙而清晰。
问题核心
Erdős #728问题关注二项式系数的素因子分解，其“中间部分”版本旨在寻找无穷多个整数三元组[k, n, m]，满足特定整除条件。
形式化目标为：对于固定常数c和d，能否找到无穷多组[k, n, m]使得[k+m choose k]能整除[2n choose n]，其中m约等于c*n^d。
Lean中的具体构造取n=2k，并设定m超过k*ln(k)一个特定的量，以此将猜想转化为可操作的形式。
转化与定理
证明的关键步骤是将目标整除性条件v_p(2k choose k) >= v_p(k+m choose k)进行等价转化。
这里的核心数学工具是库默尔定理，该定理指出v_p(n choose k)的值，等于在p进制下计算k+(n-k)时的进位次数。
因此，证明问题被转化为：需要证明对于所构造的无穷多个k，对于每个素数p，k+m加k时的进位次数至少等于k加k时的进位次数。
大小素数分治
证明策略根据素数p的大小分为两种情况。对于大素数p>ln(k)，证明使用了一个“强制进位”引理：如果k远大于p，那么k+(k+m)的p进制加法必然会产生至少floor(k/p)次进位。
对于小素数，情况更复杂，因为连续整数中可能包含多个p的倍数，无法直接套用简单引理。这需要引入更精妙的分析工具来处理小素数对整除性的贡献。
概率与排除
对于小素数，AI的证明引入了概率论思想。它论证对于一个“随机”的k，其在p进制下的数字分布几乎是均匀的，因此能产生足够多的进位。
证明的重点是排除那些可能导致进位不足的“坏”k值，即k含有异常高的p幂因子的情况。通过切尔诺夫（Chernoff）界限和并集界限，Lean代码形式化地证明了这种“坏”k的出现概率极低，从而保证了必有无穷多个“好”k满足所有素数的整除条件。
AI解决Erdős问题的过程，展示了其将抽象问题转化为结构化步骤并进行严谨论证的能力。这预示着AI将成为未来数学研究的强大辅助工具，而非简单的计算器。AI的下一个数学突破会在哪个领域？
