Erdős问题的形式化

摘要

本客座文章由Boris Alexeev撰写，介绍围绕Erdős问题的近期进展，特别是利用人工智能对旧新数学进行形式化。背景：保罗·埃尔德什提出了大量猜想，Thomas Bloom于2023年5月建立erdosproblems.com跟踪进展。2025年8月添加论坛，2025年5月Google DeepMind启动形式化猜想项目。Bloom和陶哲轩提议将网站与OEIS链接。目前网站上有1100多个问题，约40%已解决，约240个问题在Lean中形式化，17个有形式化解，260个链接到OEIS。文章还提及人类无AI形式化的早期例子，如Bloom和Mehta形式化单位分数问题。