Terence Tao / Erdős Problems
The New Workflow
AI不仅解决了Erdős #728问题，更建立了从自然语言证明到Lean形式化验证，再回译为更优自然语言的“乒乓式”迭代闭环。这种交互填补了逻辑间隙,重塑了数学证明范式。
核心变革在于AI赋予了文本极速重写与定制阐述的能力。数学论文不再是静态的孤本，而是可以针对不同受众，瞬间生成多种严谨度与叙事结构的“高重数”动态制品。
“比起解题本身，更令人着迷的是AI驱动下数学文本的极速重写与动态阐述能力——这标志着‘高重数’论文时代的到来。”
Erdős问题的原始表述存在歧义。AI在初步尝试中发现了平凡解，促使人类研究者引入新约束 \(a,b \le (1-\varepsilon)n\)，从而排除了琐碎情况，重新确立了问题预期的精神内核与边界。
ChatGPT在调整后的约束条件下，率先给出了常数 C 取较小值时的证明。尽管后续发现文献中已有类似结论，但这开启了从模糊自然语言到精确数学逻辑的关键转化步骤。
AI工具Aristotle成功将自然语言证明转化为Lean代码。这种形式化验证不仅确认了逻辑的绝对正确性，还反过来自动修复了原证明中的微小错误，实现了“验证即修正”。
通过将Lean证明重新输入ChatGPT，AI生成了更易读的自然语言版本。经多轮对话打磨，填补了逻辑跳跃，使其接近人类写作的流畅度，实现了机器语言向人类语言的高质量回归。
AI进一步调整论证结构，成功同时处理了常数 C 为大值和小值的情况。这种在不同参数设定间灵活切换证明路径的能力，展示了其在处理复杂数学逻辑结构中惊人的适应性。
传统论文修改耗时费力，而AI允许针对不同受众快速生成多种阐述版本。未来的核心论文将不再单一，而是伴随大量由AI生成的、具有不同侧重点和详细程度的“卫星版本”。