陶哲轩：AI让数学进入「工业化」时代，数学家也可以是「包工头」

Core Insights - The article discusses the transformation of mathematical research, driven by AI and formal proof languages like Lean, moving away from traditional methods towards a more industrialized approach [1][2]. Group 1: Transformation of Mathematical Research - Terry Tao highlights that traditional mathematical research is facing a paradigm shift due to the integration of AI and formal proof systems, which reduce repetitive tasks and enhance collaboration [2][5]. - The use of large language models (LLMs) and automated formalization is making tedious tasks easier, allowing mathematicians to focus on more complex problems [2][9]. - The modularization of research is expected to enable non-experts, or "citizen mathematicians," to contribute to advanced research, thereby accelerating progress in the field [2][29]. Group 2: Changes in Collaboration and Roles - The article suggests that the future of mathematics may resemble software engineering, with roles such as "architects" or project managers emerging to oversee large collaborative projects [2][23]. - Tao emphasizes the importance of collaboration, noting that the traditional model of individual research is insufficient for the complexity of modern mathematical problems [25][26]. - The integration of formal tools and AI is expected to facilitate seamless collaboration among individuals with varying skill sets, allowing for a more efficient division of labor in mathematical research [27][28]. Group 3: Impact of Formalization on Mathematical Thinking - Formalization is changing the way mathematicians think, helping them identify implicit assumptions and refine their definitions, which leads to clearer and more concise writing [10][12]. - The process of formalization encourages a new style of proof writing that is more modular and easier to understand, contrasting with traditional linear proofs [12][13]. - Tao notes that formalization allows for a more precise understanding of the applicability of mathematical tools, potentially leading to breakthroughs in various areas [15][16]. Group 4: Future of Mathematical Research - The article predicts a future where the role of mathematicians will expand to include project management and coordination of large-scale research efforts, rather than solely focusing on individual contributions [29][30]. - As tools and collaboration methods evolve, the barriers to entry for participating in mathematical research are expected to decrease, allowing a broader range of individuals to engage in the field [30][31]. - The potential for AI to handle repetitive tasks in mathematical research is seen as a way to unlock new levels of productivity and creativity among mathematicians [32][34].