陶哲轩携AI再战数学！o4-mini秒怂弃赛，Claude 20分钟通关

新智元报道编辑：桃子陶哲轩 YouTube 视频第二弹震撼来袭！这一次，他让 AI 挑战在 Lean 中形式化代数蕴含证明，结果 Claude 约 20 分通关，o4-mini 太过谨慎直接「弃赛」。 3 天后，陶哲轩 YouTube 视频二更来了。这次，他尝试了一种更短、更概念化的证明版本，