【新智元导读】陶哲轩YouTube视频第二弹震撼来袭！这一次，他让AI挑战在Lean中形式化代数蕴含证明，结果Claude约20分通关，o4-mini太过谨慎直接「弃赛」。

3天后，陶哲轩YouTube视频二更来了。

这次，他尝试了一种更短、更概念化的证明版本，并测试Claude、o4-mini能否基于之前的非形式和形式证明，生成类似的形式化代码。

实验的核心是，在Lean中形式化同一个代数蕴含的证明。

此外，他还发文深入剖析了，自动化工具不同尺度上的效率表现，以及自动化与人工干预之间的微妙平衡。