b*******8
发帖数: 37364 | 1 【 以下文字转载自 Programming 讨论区 】
发信人: Caravel (克拉维尔), 信区: Programming
标 题: Google AI system proves over 1200 mathematical theorems
发信站: BBS 未名空间站 (Thu Jun 20 13:46:56 2019, 美东)
Google AI system proves over 1200 mathematical theorems
A new and remarkable development here is that several researchers at Google
’s research center in Mountain View, California have now developed an AI
theorem-proving program. Their program works with the HOL-Light theorem
prover, which was used in Hales’ proof of the Kepler conjecture, and can
prove, essentially unaided by humans, many basic theorems of mathematics.
What’s more, they have provided their tool in an open-source release, so
that other mathematicians and computer scientists can experiment with it.
The Google AI system was “trained” on a set of 10,200 theorems that the
researchers had gleaned from several sources, including many sub-theorems of
Hales’ proof of the Kepler conjecture. Most of these theorems were in the
area of linear algebra, real analysis and complex analysis, but the Google
researchers emphasize that their approach is very broadly applicable.
In the initial release, their software was able to prove 5919, or 58% of the
training set. When they applied their software to a set of 3217 new
theorems that it had not yet seen, it succeeded in proving 1251, or 38.9%.
Not bad for a brand-new piece of software…
Mathematicians are already envisioning how this software can be used in day-
to-day research. Jeremy Avigad of Carnegie Mellon University sees it this
way: |
b*******8
发帖数: 37364 | |
i********r
发帖数: 12113 | 3 能证明现在人类还无法证明的理论那就是真牛逼了
【在 b*******8 的大作中提到】
: 将军们议议
|
o***o
发帖数: 194 | |
c*****t
发帖数: 10738 | 5 用处不是很大。基本上就是在以前的证明手段的空间里搜索。真正得难题，需要得是石
破天惊得新手段。 |
b*******8
发帖数: 37364 | 6 要能独立提出理论那就牛逼了。比如给它方程，自己就发现五次以上没有解析解，而且
发明群论证明之。
【在 i********r 的大作中提到】
: 能证明现在人类还无法证明的理论那就是真牛逼了
|
b*******8
发帖数: 37364 | 7 如果只是在人类定义好的公理体系内证明定理，那的确意义不大，取决于人类是否已经
把形式化做好。
【在 c*****t 的大作中提到】
: 用处不是很大。基本上就是在以前的证明手段的空间里搜索。真正得难题，需要得是石
: 破天惊得新手段。
|
i********r
发帖数: 12113 | 8 那就更牛逼了。说到底现在的AI只会解决有套路的问题，属于比较低级的阶段，真正替
代人类还早的很
【在 b*******8 的大作中提到】
: 要能独立提出理论那就牛逼了。比如给它方程，自己就发现五次以上没有解析解，而且
: 发明群论证明之。
|
V*******n
发帖数: 1 | 9 不知道AI如何能通过已经做好的证明学习证明数学定理，尤其是充满”显然“，”平庸
“这类词汇的证明，是不是AI给的证明也有很多不显然的”显然“？ |
o***o
发帖数: 194 | 10 现在AI是算命，你要给它一个算命模板
谷歌还能跳出算命圈子，算命理论就是谷歌特有的 |
T*******x
发帖数: 8565 | 11 显然，任何一个偶数都等于两个素数之和。
【在 V*******n 的大作中提到】
: 不知道AI如何能通过已经做好的证明学习证明数学定理，尤其是充满”显然“，”平庸
: “这类词汇的证明，是不是AI给的证明也有很多不显然的”显然“？
|
C*****l
发帖数: 1 | 12 机器定理推导本质上应该时可能的，目前的问题是不知道以怎样的形式来输入人类的知
识。Stephen Wolfram提出了computable knowledge的概念，但是也没有很好的办法。
【在 b*******8 的大作中提到】
: 将军们议议
|
d****o
发帖数: 32610 | 13 估计这些定理就是习题水平
Google
【在 b*******8 的大作中提到】
: 如果只是在人类定义好的公理体系内证明定理，那的确意义不大，取决于人类是否已经
: 把形式化做好。
|
