子群

本文介绍了著名数学家陶哲轩在社交网络上宣布成功完成多项式Freiman-Ruzsa猜想（PFR）的形式化证明项目，耗时仅三周，证明得到了Lean编译器的认可。猜想符合标准公理，展示了计算机和人工智能辅助证明的成功。文章详细介绍了这一数学成就及其形式化工作，并解释了多项式Freiman-Ruzsa猜想...