Translated data: Tao Chexian successfully formalized the proof of the Polynomial Freiman-Ruzsa Conjecture using AI tools, marking a wide application of artificial intelligence in mathematical research and causing a stir in the mathematical community. In his blog post, he detailed the process of formalizing the proof using Blueprint in Lean4. This project, spanning three weeks, successfully achieved the formalization of the Polynomial Freiman-Ruzsa Conjecture, astonishing people with the power of artificial intelligence in mathematical research.