https://www.zhihu.com/question/1913003206876853004/answer/1915201140573836227

为了最大噱头以吸引大众眼球、引诱全球范围跟进、并使其在编程等更实用领域达到「可用」程度让风投快速回本，AI圈在疫情前放弃了谷歌的游戏领域（记得阿尔法狗否？），选择了「通用」领域。

还记得疫情前就见新闻号称某AI做高考数学卷得了一百三十多，为何这几年闭口不提了呢？

陶哲轩的 不等式证明工具 用的是远在这十年AI潮兴起之前的技术、工具和算法，不需任何所谓大模型和训练过程，即便还远未充分优化也在多数情况下具备秒级的响应时间，更无需任何昂贵硬件，不更接近简约低能耗的「智能」吗？

开始证明。当前情况：
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3*z + 1
求证：x < 7*z + 2
检验以下不等式可否成立：
1*x > 0
1*x + -2*y < 0
1*y > 0
1*y + -3*z < 1
1*z > 0
1*x + -7*z >= 2
以下式子取和，得证不可能成立：
1*x + -2*y < 0 两边乘 -1/4
1*y + -3*z < 1 两边乘 -1/2
1*z > 0 两边乘 1/4
1*x + -7*z >= 2 两边乘 1/4
证明完毕！

对当下风行的对话式ai叹为观止的，不妨看看简单的对话机器人在几十年前就可如何通过图灵测试再想想为何其不再被提及。

搞懂「鸟」，相比搞懂不等式证明，哪个是更值得当下投入的「智能」，每个投入学术和职场生涯、以及晚来的投资者该三思后行