如果把一些现有的、没有审查过的结果直接当成引理放进去用的话，也会存在问题。之前不就有人拿Lean说证了个什么定理，结果一看默认那个定理的等价命题是成立的 ^-^

我也认为目前的数学工具还不足以解决，大多数人都偏向于AI是个能力的凸包，感觉更像是A\在烂炒，或许还是需要再等等。