形式化证明相关资讯

数学家恨AI，却戒不掉它

强大的人工智能模型正在给数学这门古老学科带来存在性风险：它可能掏空人们对证明的理解，重塑学术评价与荣誉分配。但矛盾在于，几乎没有人能真正停下使用它——因为AI实在太好用了。本文梳理数学家与AI之间这场爱恨交织的拉锯战：从形式化证明工具到自动