昨晚开始，搞到两三点，今天早上继续。使用AI左右手互搏的方式，推广上世纪里一个非常重要的定理。不是通过设置不同的智能体来完成这个任务，而是转换到不同环境进行评估，我会仔细检查评估的结果，再添加自己的意见。

最初，AI提供了一个错误的版本，张冠李戴，另一个AI评审发现了其中的几个关键性陈述的错误（证明本身经过Lean检验过没有问题），之后另一个AI工具做了修改改进，我也介入提了几个评论与改进方向。经过几轮优化，最终得到两套东西，包括了几个引理、定理与一些特例。一套是原始定理弱化之后的变形的版本，一套是忠实于原始定理的版本，但是AI投机取巧，直接把原始定理的结果作为一个基本公理了——这显然不是我想要的，尽管原则上似乎也没有大问题。整体上，第一套有自己的一点价值，第二套还需要仔细检查才能确定是否有一点价值。

整个流程下来，在步骤不多的证明中，AI可以很好地完成任务，但是大幅的跳跃，还是需要人来掌控，并且AI可能会投机取巧避开难的任务。