Core Viewpoint - DeepMind has launched an open-source formal mathematical conjecture library, which includes a collection of formally stated mathematical conjectures, addressing the scarcity of resources for open conjectures and aiding AI models in enhancing mathematical reasoning and proof capabilities [1][6][8]. Group 1 - The conjecture library contains a diverse set of mathematical conjectures formalized using Lean, sourced from various avenues [9]. - The library serves as a formal "exercise set" for computers, allowing traditional automated theorem proving (ATP) systems to conduct proof searches based on the conjectures within [11][12]. - Users can contribute by formalizing new conjectures, suggesting desired formal problems, improving citations, and correcting inaccuracies in existing formalizations [16][17][18]. Group 2 - The library is expected to become a benchmark for testing automated theorem proving or formal tools, thereby assisting AI models in improving their mathematical reasoning and proof capabilities [7][8]. - The collaboration between DeepMind and mathematician Terence Tao has been significant, with Tao endorsing the potential of AI in mathematical discovery [28][29]. - The AlphaEvolve project, developed by DeepMind, has made strides in solving long-standing geometric challenges, demonstrating the potential of AI in mathematics [35][41].