李诞呼吁数学界Lean化证明并用AI智能体批量产出新证明

李诞再次呼吁数学学术界完成四步：把已有数学证明和论文全部Lean化，用高强度agent黑灯工厂批量产出新的Lean证明，构建全新数学工具与体系，并由教授带领PhD、本科生、中学生全民参与。Dr. Yin 补充设想，远AI时代的数学文献将以类似LLM token向量空间的网络结构存在，数学工作的重要性取决于其对这张网络的改变程度。