日志
无语了
热度 10
这段时期在做一个大的证明。已经把框架和几个主要目标证完了，让AI帮忙把最后一个目标的对应引理写出来。
AI很快给出了引理的内容和证明梗概，我想着最后一个目标跟前面几个目标相似，前面AI表现的还是很可靠的，就没仔细看引理的内容是否完全正确。
用了两天的时间在AI的帮助下把这个引理证完了，证的时候还挺麻烦的。
然后戏剧性的一幕出现了。AI告诉我，这个引理和预期的引理不完全相同，最后的证明用不上。
我质问AI，这个引理不是你给出的吗，为什么会不匹配？AI避而不答，只是告诉我新的引理如何如何，特别容易证明之类的。
惨痛的教训呀。
