On the 6th, our reporter discovered that the AI4Math team, comprising members from Professor Dong Bin's research group at the Beijing International Center for Mathematical Research at Peking University, along with their collaborators, has successfully cracked an open problem in commutative algebra—the Anderson Conjecture. This achievement was made possible through the utilization of a self-developed automated AI framework. Furthermore, the team executed roughly 19,000 lines of formal verification using Lean, a programming language and theorem prover specifically designed for the formal verification of mathematical theorems. This event signifies a pioneering moment in China, where an AI framework has been employed to address a complex issue in commutative algebra and accomplish extensive formal verification, thereby paving a novel path for the profound integration of mathematics and AI.