C*****l
发帖数: 1 | 1 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: |
C*****l
发帖数: 1 | 2 如果不计成本，能不能把所有数学的knowledge都输入电脑（当然是computable的形式
）吗？
。 |
c*******v
发帖数: 2599 | 3 Did they try the RH? P and NP?
Google
of
【在 C*****l 的大作中提到】
: 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
|
C*****l
发帖数: 1 | 4 黎曼猜想可以试试，PNP其实最大的问题是没办法formulate question。其实人做数学
，我观察其实人做数学除了推理，枚举很重要，老邱说他为了证明卡拉比猜想，尝试了
1000多种函数，这说明计算机如果掌握了数学知识，也可以做研究。
但是人类的数学知识内容还是太丰富了，不知道怎么才能很好的输入
【在 c*******v 的大作中提到】
: Did they try the RH? P and NP?
:
: Google
: of
|
R******e
发帖数: 623 | 5 定理机器证明已经没多大意思了，有了Tarski等人的结果，加以王浩的定理证明程序，
基本就是个小修小补的领域。
Google
of
【在 C*****l 的大作中提到】
: 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
|
C*****l
发帖数: 1 | 6 还差得远呢，机器证明本质上可以替代人类来发现新的定理。
【在 R******e 的大作中提到】
: 定理机器证明已经没多大意思了，有了Tarski等人的结果，加以王浩的定理证明程序，
: 基本就是个小修小补的领域。
:
: Google
: of
|
a*****g
发帖数: 19398 | 7 有趣哦
Google
of
【在 C*****l 的大作中提到】
: 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
|
m******r
发帖数: 1033 | 8 那数学系教授可以用它来写paper ? 发表 ？ 反正别人也不知道这定理是你想的， 还
是机器想的。 |
m********5
发帖数: 17667 | 9 关键是形式化，这一步很花时间
【在 R******e 的大作中提到】
: 定理机器证明已经没多大意思了，有了Tarski等人的结果，加以王浩的定理证明程序，
: 基本就是个小修小补的领域。
:
: Google
: of
|
g****t
发帖数: 31659 | 10 有。一個例子是嚴格證明羅倫茲系統是混沌。但是作者的phd論文有bug（不是程序bug)
。後來修了另一個版本。他的phd論文我多年前看過。後來那個版本沒看。
另一個例子是開普勒裝球問題。發在annals。但是審稿人說論文是對的；不保證程序沒
bug。
這個領域很實用。等於是處理大規模電路的邏輯驗證。所以intc等公司有這專業的人。
還有半導體的tool software也有。
: 那数学系教授可以用它来写paper ? 发表 ？ 反正别人也不知道这定理是你想的
， 还
: 是机器想的。
【在 m******r 的大作中提到】
: 那数学系教授可以用它来写paper ? 发表 ？ 反正别人也不知道这定理是你想的， 还
: 是机器想的。
|
|
|
w***g
发帖数: 5958 | 11 这个方向大有可做, 就是没有funding.
bug)
【在 g****t 的大作中提到】
: 有。一個例子是嚴格證明羅倫茲系統是混沌。但是作者的phd論文有bug（不是程序bug)
: 。後來修了另一個版本。他的phd論文我多年前看過。後來那個版本沒看。
: 另一個例子是開普勒裝球問題。發在annals。但是審稿人說論文是對的；不保證程序沒
: bug。
: 這個領域很實用。等於是處理大規模電路的邏輯驗證。所以intc等公司有這專業的人。
: 還有半導體的tool software也有。
:
:
: 那数学系教授可以用它来写paper ? 发表 ？ 反正别人也不知道这定理是你想的
: ， 还
:
: 是机器想的。
|
g****t
发帖数: 31659 | 12 跟集成电路设计的tool关系非常密切。过去十几年，中国08以来，至少几万亿做
集成电路。但是路线是用别人的tool，早出结果报成果。现在知道缺tool了。
【在 w***g 的大作中提到】
: 这个方向大有可做, 就是没有funding.
:
: bug)
|
p***o
发帖数: 1252 | 13 没有funding就慢慢做，PDR/IC3也做了快10年了。
【在 w***g 的大作中提到】
: 这个方向大有可做, 就是没有funding.
:
: bug)
|
h*********3
发帖数: 1 | 14 有哥德尔不完备定理挡前面呢
【在 C*****l 的大作中提到】
: 如果不计成本，能不能把所有数学的knowledge都输入电脑（当然是computable的形式
: ）吗？
: 。
|
C*****l
发帖数: 1 | 15 歌德尔是说任何公理体系里面都有不可判定的定理，并没有说这样的定理有多少
【在 h*********3 的大作中提到】
: 有哥德尔不完备定理挡前面呢
|
R******e
发帖数: 623 | 16 是推导出的定理，不是发现定理，就跟程序跑出结果一样，没有多少趣味。
【在 C*****l 的大作中提到】
: 还差得远呢，机器证明本质上可以替代人类来发现新的定理。
|
R******e
发帖数: 623 | 17 为啥没房顶？就是因为行家知道不可做了。
程序的正确性证明，很容易就成为np难问题，小规模的输入还可以，集成电路那个规模
，就只好想想了。
【在 w***g 的大作中提到】
: 这个方向大有可做, 就是没有funding.
:
: bug)
|
R******e
发帖数: 623 | 18 好好的不完备定理被你们说得跟笑话一样。
完备的也就是任何命题都可以判定的公理体系很多，比如欧式几何等等。
公理体系必须丰富到包含一阶皮亚诺算术，必须无矛盾或者一致，然后才有命题不可判
定。
即使可判定的公理体系也有复杂度为npc的判定问题，比如布尔逻辑范式命题的赋值问
题。
【在 C*****l 的大作中提到】
: 歌德尔是说任何公理体系里面都有不可判定的定理，并没有说这样的定理有多少
|
R******e
发帖数: 623 | 19 设计芯片的软件或者工具的公司有做定理机器证明的，无非就是把已有的结果用上，指
望有突破是不可能的，就是小规模的或者p复杂度的可以，其他的免谈。没有，不可以
，有也不指望有多大作用。 |
R******e
发帖数: 623 | 20 Tarski的结果和Grobner等人的算法经常就是指数级别的，大多数时候就是看看而已。
这个领域的人，缺了不行，大用也是浪费。就这现状，大家归安吧。 |
|
|
C*****l
发帖数: 1 | 21 本质上没有不可逾越的鸿沟，定理要证明了才能叫定理，如果电脑可以证明或者证伪大
量给定定理，就可以让电脑生成新定理，再去证明。
【在 R******e 的大作中提到】
: 是推导出的定理，不是发现定理，就跟程序跑出结果一样，没有多少趣味。
|
C*****l
发帖数: 1 | 22 行家根本不作数，搞神经网络那几位几十年就靠几十万的小funding勉强维持，最后还
是那些重金投入的方向被这个方向打败
【在 R******e 的大作中提到】
: 为啥没房顶？就是因为行家知道不可做了。
: 程序的正确性证明，很容易就成为np难问题，小规模的输入还可以，集成电路那个规模
: ，就只好想想了。
|
x****u
发帖数: 44466 | 23 因为tool可以盗版，不怕国外封锁
【在 g****t 的大作中提到】
: 跟集成电路设计的tool关系非常密切。过去十几年，中国08以来，至少几万亿做
: 集成电路。但是路线是用别人的tool，早出结果报成果。现在知道缺tool了。
|
R******e
发帖数: 623 | 24 读读开辟新领域的定理的证明就知道了，那不是计算机能证明的。
依照Godel定理，必须添加新公理，才能有有趣味的定理产生出来，否则就是跑程序而
已。
数学不该看作定理的证明，它是靠人的直觉和准形式化的方法构建的真命题的集合。
【在 C*****l 的大作中提到】
: 本质上没有不可逾越的鸿沟，定理要证明了才能叫定理，如果电脑可以证明或者证伪大
: 量给定定理，就可以让电脑生成新定理，再去证明。
|
R******e
发帖数: 623 | |
C*****l
发帖数: 1 | 26 直觉是靠不住的，给人类神秘的虚荣感觉，就好比以前围棋高手也说是靠直觉，其实就
是一种计算而已。一个简单的类比，一个数学定理可不可以通过自然语言解释给别人听
，当然是可以得。既然是可以得，为啥不能建立基于自然语言的计算？
【在 R******e 的大作中提到】
: 读读开辟新领域的定理的证明就知道了，那不是计算机能证明的。
: 依照Godel定理，必须添加新公理，才能有有趣味的定理产生出来，否则就是跑程序而
: 已。
: 数学不该看作定理的证明，它是靠人的直觉和准形式化的方法构建的真命题的集合。
|
R******e
发帖数: 623 | 27 不用这么辩解，拿个实例来吧：比如从欧几里德几何到非欧几何，这个应该是计算机做
不到的，怎么证明第五公设是独立的？
复几何和理想、素数之间的关系咋找出来？
再随便举个例子：一般意义上的发散级数可启发不同可和性的定义，你让计算机做？
看看数学史，每一次大定理的证明，都不是靠形式化能解决的，都有直觉。
【在 C*****l 的大作中提到】
: 直觉是靠不住的，给人类神秘的虚荣感觉，就好比以前围棋高手也说是靠直觉，其实就
: 是一种计算而已。一个简单的类比，一个数学定理可不可以通过自然语言解释给别人听
: ，当然是可以得。既然是可以得，为啥不能建立基于自然语言的计算？
|
R******e
发帖数: 623 | 28 恰巧RH不好形式化，而P=NP形式化得差不多了。我纳闷你们形式化的定义是啥。
【在 C*****l 的大作中提到】
: 黎曼猜想可以试试，PNP其实最大的问题是没办法formulate question。其实人做数学
: ，我观察其实人做数学除了推理，枚举很重要，老邱说他为了证明卡拉比猜想，尝试了
: 1000多种函数，这说明计算机如果掌握了数学知识，也可以做研究。
: 但是人类的数学知识内容还是太丰富了，不知道怎么才能很好的输入
|
R******e
发帖数: 623 | 29 反推数学就是reverse math基本就是探索哪部分数学需要多强的公理体系，事实上全部
现代数学不可能递归公理化，这已经是常识。
再说一遍，全部数学不等同证明定理
【在 h*********3 的大作中提到】
: 有哥德尔不完备定理挡前面呢
|
R******e
发帖数: 623 | 30 弄明白这两个方向的基本知识就知道两者不可比。
【在 C*****l 的大作中提到】
: 行家根本不作数，搞神经网络那几位几十年就靠几十万的小funding勉强维持，最后还
: 是那些重金投入的方向被这个方向打败
|
|
|
x****u
发帖数: 44466 | 31 阿法狗也是直觉
机器现在只有直觉，逻辑推理还得靠传统方法
【在 C*****l 的大作中提到】
: 直觉是靠不住的，给人类神秘的虚荣感觉，就好比以前围棋高手也说是靠直觉，其实就
: 是一种计算而已。一个简单的类比，一个数学定理可不可以通过自然语言解释给别人听
: ，当然是可以得。既然是可以得，为啥不能建立基于自然语言的计算？
|
C*****l
发帖数: 1 | 32 阿法狗不是仅仅靠直觉，神经网络是直觉，但是模特卡罗树搜索是很严谨的求证过程。
【在 x****u 的大作中提到】
: 阿法狗也是直觉
: 机器现在只有直觉，逻辑推理还得靠传统方法
|
C*****l
发帖数: 1 | 33 不要这么狭窄地看待计算机，如果人类可以基于联想，类比，扩展发现新的理论，电脑
本质上也可以。问题是现在表征问题的方法比较死板，自然语言其实这个时候更厉害。
【在 R******e 的大作中提到】
: 不用这么辩解，拿个实例来吧：比如从欧几里德几何到非欧几何，这个应该是计算机做
: 不到的，怎么证明第五公设是独立的？
: 复几何和理想、素数之间的关系咋找出来？
: 再随便举个例子：一般意义上的发散级数可启发不同可和性的定义，你让计算机做？
: 看看数学史，每一次大定理的证明，都不是靠形式化能解决的，都有直觉。
|
R******e
发帖数: 623 | 34 原来你是做哲学的，我输了。
【在 C*****l 的大作中提到】
: 不要这么狭窄地看待计算机，如果人类可以基于联想，类比，扩展发现新的理论，电脑
: 本质上也可以。问题是现在表征问题的方法比较死板，自然语言其实这个时候更厉害。
|
x****u
发帖数: 44466 | 35 蒙特卡洛树一直就有，阿法狗的突破时机器直觉
【在 C*****l 的大作中提到】
: 阿法狗不是仅仅靠直觉，神经网络是直觉，但是模特卡罗树搜索是很严谨的求证过程。
|
c*******v
发帖数: 2599 | 36 有个文章讲RH可以等价成一个只用非常简单的逻辑的不等式来进行验证。
我以前写过程序。非常慢。远不如现有的siegel／图灵／黎曼算法。
但是这证明了RH可以简化为一个非常简单的计算机程序的停机问题。
也就是可以形式化。
【在 R******e 的大作中提到】
: 恰巧RH不好形式化，而P=NP形式化得差不多了。我纳闷你们形式化的定义是啥。
|
R******e
发帖数: 623 | 37 你说的是王浩《数理逻辑通俗讲话》里关于RH的那个命题吧？那是一个穷举，如果RH成
立，就会一路跑下去，永远不停机。没意义的。那不叫数学证明，只能叫数值计算或者
数值验证。
定理的机器证明步骤应该是finite的，尽管是指数级别甚至是更高。
【在 c*******v 的大作中提到】
: 有个文章讲RH可以等价成一个只用非常简单的逻辑的不等式来进行验证。
: 我以前写过程序。非常慢。远不如现有的siegel／图灵／黎曼算法。
: 但是这证明了RH可以简化为一个非常简单的计算机程序的停机问题。
: 也就是可以形式化。
|
c*******v
发帖数: 2599 | 38 没人讲RH有数学证明。
我讲的是RH可以形式化成很低阶的逻辑。不需要复数以及黎曼函数。
也不需要转成随机矩阵什么的。
我记得最后就是整数可以拆分成几种因式分解这种组合数学的不等式。有用到log。
文章只有几页，但是我不知道是不是被检查过。
http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
【在 R******e 的大作中提到】
: 你说的是王浩《数理逻辑通俗讲话》里关于RH的那个命题吧？那是一个穷举，如果RH成
: 立，就会一路跑下去，永远不停机。没意义的。那不叫数学证明，只能叫数值计算或者
: 数值验证。
: 定理的机器证明步骤应该是finite的，尽管是指数级别甚至是更高。
|
c*******v
发帖数: 2599 | 39 多年前在国内,看到普渡有个教授，公布自己证明了RH。我还研究过它的文章。
后来去外国网站一看，说这哥们每隔几年就给一个谁也看不懂错误证明。就靠这一手拿
NSF的钱不
间断的。
【在 c*******v 的大作中提到】
: 没人讲RH有数学证明。
: 我讲的是RH可以形式化成很低阶的逻辑。不需要复数以及黎曼函数。
: 也不需要转成随机矩阵什么的。
: 我记得最后就是整数可以拆分成几种因式分解这种组合数学的不等式。有用到log。
: 文章只有几页，但是我不知道是不是被检查过。
: http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
: www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
|
R******e
发帖数: 623 | 40 还没看，如果是RH的机器证明程序，错的概率极高。
【在 c*******v 的大作中提到】
: 没人讲RH有数学证明。
: 我讲的是RH可以形式化成很低阶的逻辑。不需要复数以及黎曼函数。
: 也不需要转成随机矩阵什么的。
: 我记得最后就是整数可以拆分成几种因式分解这种组合数学的不等式。有用到log。
: 文章只有几页，但是我不知道是不是被检查过。
: http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
: www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
|
|
|
R******e
发帖数: 623 | 41 服了你了，有复数未必就复杂。
你的低阶逻辑能低到多少？
你逗人玩。
那文章跟定理的机器证明或RH的形式化没有丝毫关系，咣当！
【在 c*******v 的大作中提到】
: 没人讲RH有数学证明。
: 我讲的是RH可以形式化成很低阶的逻辑。不需要复数以及黎曼函数。
: 也不需要转成随机矩阵什么的。
: 我记得最后就是整数可以拆分成几种因式分解这种组合数学的不等式。有用到log。
: 文章只有几页，但是我不知道是不是被检查过。
: http://www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
: www.math.lsa.umich.edu/~lagarias/doc/elementaryrh.pdf
|
c*******v
发帖数: 2599 | 42 这种逻辑复杂程度的刻画叫做"Pi one sentence".
历史上有人做过的。
RH本身是严格的数学猜想，怎么会有形式化问题。
有问题的是可以简化到只用哪几个符号。
最后你查一下我几年前写的literature programming的一点notes。我看一个问题
一般至少到那个程度的细节。在我了解的细节知识以下的道听途说，不回复了。
【在 R******e 的大作中提到】
: 服了你了，有复数未必就复杂。
: 你的低阶逻辑能低到多少？
: 你逗人玩。
: 那文章跟定理的机器证明或RH的形式化没有丝毫关系，咣当！
|
R******e
发帖数: 623 | 43 受不了了。
依照数的扩张， 得从皮亚诺公理一路到复数，你先试试。即使用非标准模型，你也得
定义出素数，积分，开拓等等吧。你先试试咋形式化这些。
至于表述为一个命题，这是个trivial的工作，只看长短而已，看来你现在不熟悉math
logic的基本知识了。
真没兴趣多说了，版上不少哲学家。
【在 c*******v 的大作中提到】
: 这种逻辑复杂程度的刻画叫做"Pi one sentence".
: 历史上有人做过的。
: RH本身是严格的数学猜想，怎么会有形式化问题。
: 有问题的是可以简化到只用哪几个符号。
: 最后你查一下我几年前写的literature programming的一点notes。我看一个问题
: 一般至少到那个程度的细节。在我了解的细节知识以下的道听途说，不回复了。
|
C*****l
发帖数: 1 | 44 难不代表不可能，stephen wolfram一直在搞这个。
As I mentioned early in this blog post, it’s going to take all sorts of new
built-in functions to capture the frameworks needed to represent modern
pure mathematics—together with lots of entity-like objects. And it’ll
certainly take years of careful design to make a broad system for pure
mathematics that’s really clean and usable. But there’s nothing
fundamentally difficult about having symbolic constructs that represent
differentiability or moduli spaces or whatever. It’s just language design,
like designing ways to represent 3D images or remote computation processes
or unique external entity references.
https://blog.stephenwolfram.com/2014/08/computational-knowledge-and-the-
future-of-pure-mathematics/
math
【在 R******e 的大作中提到】
: 受不了了。
: 依照数的扩张， 得从皮亚诺公理一路到复数，你先试试。即使用非标准模型，你也得
: 定义出素数，积分，开拓等等吧。你先试试咋形式化这些。
: 至于表述为一个命题，这是个trivial的工作，只看长短而已，看来你现在不熟悉math
: logic的基本知识了。
: 真没兴趣多说了，版上不少哲学家。
|
g****t
发帖数: 31659 | 45 RH跟初等数论不等式等价。你是不是看不懂英语文章？这是两个文章证明过的。
我有本数论书，偶尔还刷着题呢。
math
【在 R******e 的大作中提到】
: 受不了了。
: 依照数的扩张， 得从皮亚诺公理一路到复数，你先试试。即使用非标准模型，你也得
: 定义出素数，积分，开拓等等吧。你先试试咋形式化这些。
: 至于表述为一个命题，这是个trivial的工作，只看长短而已，看来你现在不熟悉math
: logic的基本知识了。
: 真没兴趣多说了，版上不少哲学家。
|
R******e
发帖数: 623 | 46 俺没看懂，俺看到文章跟机器证明或者形式化毫无关系。再摆出十个跟RH等价的初等数
学命题，也跟形式化没关系。
难道我说错了吗？
算了，给你的建议就是，你就当作爱好玩玩吧，现代数论你基本弄不懂多少，比如丢番
图几何或称算术代数几何，代数几何都看得费劲，咋弄算术代数几何？
【在 g****t 的大作中提到】
: RH跟初等数论不等式等价。你是不是看不懂英语文章？这是两个文章证明过的。
: 我有本数论书，偶尔还刷着题呢。
:
: math
|
c*******v
发帖数: 2599 | 47 初等数论不等式本身就是严格形式化的。在皮亚诺算术之内。
RH的形式化问题，你指的是什么意思？
【在 R******e 的大作中提到】
: 俺没看懂，俺看到文章跟机器证明或者形式化毫无关系。再摆出十个跟RH等价的初等数
: 学命题，也跟形式化没关系。
: 难道我说错了吗？
: 算了，给你的建议就是，你就当作爱好玩玩吧，现代数论你基本弄不懂多少，比如丢番
: 图几何或称算术代数几何，代数几何都看得费劲，咋弄算术代数几何？
|
R******e
发帖数: 623 | 48 一阶皮亚诺算术是严格形式化的，二阶的你见过几个形式化的。不过很多人分不清一阶
和二阶，出错不足为怪。我没兴趣解释基本概念。
话说，你不是不回复了吗？
【在 c*******v 的大作中提到】
: 初等数论不等式本身就是严格形式化的。在皮亚诺算术之内。
: RH的形式化问题，你指的是什么意思？
|
c*******v
发帖数: 2599 | 49 RH在PA之内是证明过的数学定理。看我给的引文你就知道了。
这回真不再继续跟你解释了。
【在 R******e 的大作中提到】
: 一阶皮亚诺算术是严格形式化的，二阶的你见过几个形式化的。不过很多人分不清一阶
: 和二阶，出错不足为怪。我没兴趣解释基本概念。
: 话说，你不是不回复了吗？
|
R******e
发帖数: 623 | 50 哪篇论文证明了RH在PA之内？
【在 c*******v 的大作中提到】
: RH在PA之内是证明过的数学定理。看我给的引文你就知道了。
: 这回真不再继续跟你解释了。
|
|
|
c*******v
发帖数: 2599 | 51 RH = a sentence like
"For all x, P(x)" where P is recursive in PA.
In the ref I provided, P is an elementary inequality.
【在 R******e 的大作中提到】
: 哪篇论文证明了RH在PA之内？
|
R******e
发帖数: 623 | 52 P is recursive in PA？P是PA里的递归谓词？里面的函数是PA里的递归函数？服了
【在 c*******v 的大作中提到】
: RH = a sentence like
: "For all x, P(x)" where P is recursive in PA.
: In the ref I provided, P is an elementary inequality.
|
