如果遇到自己能搞定的证明，那证明代码写的是洋洋洒洒，连标点符号都能给你排版好。

但是如果遇到自己搞不定的问题，那就在思维链上不停地兜圈子，最后给一份存在许多sorry填空的证明框架，并声称，这些sorry大概、可能以及差不多可以用某某方法搞定。

以前遇到这种情况，我还得去自己去深入思考，然后进行反驳。现在好了，有了另一个能力差不多的AI，那就让AI提意见就好。

另外一点就是，坚决不让AI兜圈子，不给AI偷懒的机会。如果大问题搞不定，就坚持让AI对问题进行拆分，提出更小粒度的辅助引理，然后跟其它AI对质。在证明的过程中，我经常感到恍惚，在两个AI争论的时候，好像都已通过了图灵测试。

在辅助引理拆分到某种程度后，总有一个AI会发现原有的设计里存在错误或者缺陷，然后对模型进行大改或者小改，再开始新的一轮证明。

写到最后，我怎么觉得把自己写成“周扒皮”了呢。