新未名空间

你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了

Caravel 写了： 2022年 12月 23日 21:03 你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了

最近研究机器(非AI)证明，挑战还是挺大的

用DL模型的话，怎么给定理证明建模梯度呢？

Caravel 写了： 2022年 12月 23日 21:03 你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了

看看chatGPT的证明对不对？

viewtopic.php?p=551438#p551438

（ヅ） 写了： 2022年 12月 23日 21:18 最近研究机器(非AI)证明，挑战还是挺大的

用DL模型的话，怎么给定理证明建模梯度呢？

按照NLP的路数来，证明里面的逻辑性比自然语言强，应该更容易一点。比如数学的基础就是集合轮，这个东西可以用公理化的方法一路攻击上来

Caravel 写了： 2022年 12月 23日 21:26 按照NLP的路数来，证明里面的逻辑性比自然语言强，应该更容易一点。比如数学的基础就是集合轮，这个东西可以用公理化的方法一路攻击上来

我最近看的机器证明是用SAT和SMT，这些机器对付propositional logic还是很厉害的。问题在于真实的定理，绝大多数是1st order logic.这些工具不太有效

Caravel 写了： 2022年 12月 23日 21:03 你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了

证明数学题可以，发现新定理没戏。

tfusion 写了： 2022年 12月 23日 21:35 证明数学题可以，发现新定理没戏。

你搞个猜想，让它证，不就行了。

verdelite 写了： 2022年 12月 23日 21:36 你搞个猜想，让它证，不就行了。

证不出来。

比如你给个非欧几何的定理，只告诉AI 欧式几何的公理，它证到死都证不出来。

其实哥德尔早已给机器定理证明判了死刑。以上就是一个例子。

tfusion 写了： 2022年 12月 23日 21:39 证不出来。

比如你给个非欧几何的定理，只告诉AI 欧式几何的公理，它证到死都证不出来。

其实哥德尔早已给机器定理证明判了死刑。以上就是一个例子。

chatGPT不从欧氏几何公理出发吧。假定它学了网上所有的知识。。。

训练一个数学博士型的chatGPT，其做数学题可能会比全能型的历害很多。

verdelite 写了： 2022年 12月 23日 21:42 chatGPT不从欧氏几何公理出发吧。假定它学了网上所有的知识。。。

训练一个数学博士型的chatGPT，其做数学题可能会比全能型的历害很多。

AI可以propose新公理，跳出哥德尔的陷阱

Caravel 写了： 2022年 12月 23日 23:17 AI可以propose新公理，跳出哥德尔的陷阱

基于冯诺依曼结构的计算机只知道你告诉它的东西。它想不出你不告诉它的东西。所以它没法propose公理。

tfusion 写了： 2022年 12月 23日 23:27 基于冯诺依曼结构的计算机只知道你告诉它的东西。它想不出你不告诉它的东西。所以它没法propose公理。

冯诺依曼结构只是一种计算机结构，没有限制计算机的能力，你要说图灵机还能唬唬人，但是依然不成立

Caravel 写了： 2022年 12月 23日 23:35 冯诺依曼结构只是一种计算机结构，没有限制计算机的能力，你要说图灵机还能唬唬人，但是依然不成立

就是图灵鸡。只知道你告诉它的。没法propse新公理

你们这些CS半路出家的人就是对计算机有基本认知问题

tfusion 写了： 2022年 12月 23日 23:38 就是图灵鸡。只知道你告诉它的。没法propse新公理

你们这些CS半路出家的人就是对计算机有基本认知问题

你连图灵机说不出来也好意思自称科班？

Caravel 写了： 2022年 12月 24日 00:02 你连图灵机说不出来也好意思自称科班？

尼玛这有啥说不出的？我着眼于具体计算机体系结构所以说冯诺依曼结构的

tfusion 写了： 2022年 12月 24日 00:05 尼玛这有啥说不出的？我着眼于具体计算机体系结构所以说冯诺依曼结构的

本版专门批评过这种行为：轻易否定一个Idea。当初弃婴就是代表。我自己也有过惨痛教训。

那些学到的基本原理都有成立条件。条件不同可能结论也会不同。

Caravel 写了： 2022年 12月 23日 21:03 你看看代数的证明都很短，套路可能也就那么多，AI完全有可能学会，至少可以把比较平凡的扩展都扫一遍，人类的领地会越来越少了

我也有同感。

计算机（AI）是有可能做出证明题的。很快就会有人用AI来挑战数学猜想，而且会很有成果，最起码会帮助找到思路。

例如像一堂张这样绞尽脑汁找灵感的过程，AI会大派用场，对A I来说就如打败人类围棋高手，就暴力的办法，它就是费点电而已。

这个有多少人断言围棋AI不可能赢，但是AI赢了大部分人才打脸，才明白这样也行！

现在AI做数学缺的是做数学团队做AI而已。
这个领域马上会有人搞，谁先搞谁先出成绩，各个领域的诺奖以后要看借助AI的智力是否还发给诺奖。

哥德尔定理说的是，你不能证明存在一个，或者做出一个定理证明AI，它的证明都是对的。

哥德尔不排除你可以做出定理证明AI，但是你必须一个一个读AI的证明来验证每一个定理的正确性

也就是说，这个AI就像一个数学家。所以楼主说的事情是很有可能发生的！

catoh 写了： 2022年 12月 24日 10:18 哥德尔定理说的是，你不能证明存在一个，或者做出一个定理证明AI，它的证明都是对的。

哥德尔不排除你可以做出定理证明AI，但是你必须一个一个读AI的证明来验证每一个定理的正确性

也就是说，这个AI就像一个数学家。所以楼主说的事情是很有可能发生的！

它暴力起来，一般数学家不是对手，无论是知识面广度深度再加上速度遍历所有可能（所谓的灵感也就是人类没能力全搞一遍各种可能性而已，AI只要搞的可能性多，数量级的多，人类就只有膜拜的份），那它就是数学家。一般数学家望尘莫及。

就如人类所谓的围棋高手对AI一样。