陶哲轩携AI再战数学！o4-mini秒怂弃赛，Claude 20分钟通关
陶哲轩对比Claude和o4-mini在Lean中形式化代数证明的实验结果，Claude用时约20分钟完成任务，而o4-mini因对称性问题直接弃题。实验揭示了自动化工具不同尺度上的效率表现以及与人工干预之间的微妙平衡。
Lean
未来已来？看陶哲轩如何“蒙眼狂奔”，33分钟让AI完成高难度数学形式化证明
陶哲轩分享了利用GitHub Copilot与Lean结合canonical策略的形式化数学证明实验，该实验针对Bruno Le Floch提供的一页纸等式理论证明。陶神尝试以低级别逐行方式形式化一个高度精确的“体力活”证明，并总结为AI辅助下的新范式。