最优水平

陶哲轩对比Claude和o4-mini在Lean中形式化代数证明的实验结果，Claude用时约20分钟完成任务，而o4-mini因对称性问题直接弃题。实验揭示了自动化工具不同尺度上的效率表现以及与人工干预之间的微妙平衡。