数学界巨震

要点:陶哲轩成功利用AI工具形式化多项式Freiman-Ruzsa猜想的证明，标志着数学研究中人工智能的广泛应用，引发数学界的震动。他强调数学研究者应学会正确使用AI工具，认为形式化证明的主流化有望创造出既人类可读又机器可解的证明，将数学变成一种编程。陶哲轩团队利用Blueprint工具，将证明过程分解成易于处理的部分，通过众多贡献者并行工作，成功形式化了PFR猜想。