现在DeepSeek更新了百万上下文的版本后，我又有了新玩法，当然这个玩法是Xiejin77和蚊行早就提示过的

DeepSeek现在的记忆力明显加强，比Gemini还要强。两者的脾气也不一样。Gemini对总体框架的构建比较好，但是有时候会绕圈子，另外会大量地在证明框架里用Sorry填空。DeepSeek比较硬核，能不Sorry就不Sorry。对细节的把握要比Gemini强。

那么，我就自己当做一个Agent，不断地让两者进行交互。通常的流程有两类：

一类是对一个大的模型，先让Gemini给出整体证明框架，然后让DeepSeek去审查并提建议。然后两者交互几轮，最终达到一致。在此期间确实澄清了多处我自己都没注意到的设计漏洞。

另一类是证明中间会用到的辅助引理。通常是让Gemini给出引理的表述，DeepSeek去证明。如果DeepSeek搞不定，那就说明辅助引理还是过于复杂，那就让DeepSeek提出更细节的辅助引理，反过来让Gemini去确认正确性，并给出证明。以此迭代，一般来说总会拆解到一个Slegehammer能够自动证明的程度。

我现在基本上就是动动鼠标，做一些复制粘贴的工作了。

当然，人心都是不知足的。等这个项目结束，我就准备先vibe coding，写出一个定制的Agent脚本，然后用这个Agent脚本去vibe proving了。