陶哲轩成功用AI工具形式化多项式Freiman-Ruzsa猜想的证明，标志着数学研究中人工智能的广泛应用，引发了数学界的震动。他在博文中详细记录了使用Blueprint在Lean4中形式化证明的过程。这一项目历时三周，成功实现了多项式Freiman-Ruzsa猜想的证明形式化，让人惊叹于人工智能在数学研究中的威力。