陶哲轩12年前的预言，AI帮他兑现了

陶哲轩12年前预言数学家将用计算机可理解的形式化语言取代LaTeX撰写论文，如今他通过Lean4和AI协作将其变为现实。他发起的Equational Theories项目针对约2200万个代数等式，依靠AI写证明、Lean自动核验、全球志愿者协作，48小时内完成大规模筛选，前9天进度达99.866%，第57天主项目基本完工，仅剩162个蕴含关系待收尾。