AI能证明所有数学定理吗？
How to Formalize All of Mathematics
面对OpenAI在数学证明领域的突破，我们既兴奋又忧虑。虽然AI在形式化证明上表现卓越，但盲目追求快速将全部数学形式化可能适得其反。我们曾目睹Math, Inc.尝试利用AI形式化Maryna Viazovska的球体堆积结果，最终发现清理AI生成的代码成本过高，不如重做。真正的价值在于高质量的形式化，而非数量。我们呼吁在AI辅助下，谨慎推进数学的形式化进程，确保其真正助力数学探索，而非浪费资源或造成损害。
如果做得好，大规模协调的形式化工作将极大地扩展数学的探索与发现；如果做得不好，轻则浪费资源，重则造成持久伤害。