Google AI system proves over 1200 mathematical theorems - 未名空间MITBBS历史存档

国际科技财经博客移民网络热点娱乐民生时事公众号

Redian新闻

>未名空间

>Programming - 葵花宝典

Google AI system proves over 1200 mathematical theorems

Google AI system proves over 1200 mathematical theorems# Programming - 葵花宝典

s*t2019-06-20 07:06

1 楼

现在手上有一个NSF的3年的grant，每年materials/supplies 的budget大概是$7000左
右，第一年我就老老实实的吧这$7000钱买材料了。现在还剩$14,000，算上overhead的
话大概还有$21,000左右。现在项目进行到一半需要买一个小的仪器，大概$20,000。我
想问的是我能不能够用这个本来买materials/supplies的钱去买这个小仪器。如果可以
的话就相当于节约了我$7000 的 overhead，然后我用我自己的startup的钱买
materials/supplies就行了，反正startup的钱没有overhead.
1.这样做的话学校会不会不高兴，因为他们就少了$7000 的 overhead赚。
2.对NSF来说他们会在乎吗？反正我会继续用我的startup的钱买materials/supplies。
每年report时候他们会检查钱到底花在什么地方了吗？我需不需要要写一个
justification来说明这样做确实有利于这个项目？在我看来这个确实是好事啊，唯一
有点吃亏的可能是学校。
请有过类似经历的同修们给点建议把。多谢!

C*l2019-06-20 07:06

2 楼

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:

l*l2019-06-20 07:06

3 楼

你要这样做，需要系里面和学校的财务帮你。可是你想想，他们这样做减少的是自己（
学校）的收
入而便宜的是你，所以politically incorrect。这是只有你一个人得利的时，没人会
愿意帮你的。系主任，dean知道了都不会高兴。
劝你不要为了这几千块去投机取巧，给自己找不必要的麻烦，不值。还是把精力放在找
更多的钱上吧。

C*l2019-06-20 07:06

4 楼

如果不计成本，能不能把所有数学的knowledge都输入电脑（当然是computable的形式
）吗？
。

L*s2019-06-20 07:06

5 楼

一般材料仪器不好互相转吧？
但是材料付学生什么的可以。NSF允许有点浮动。不过这个以后会改。

【在 l*******l 的大作中提到】

: 你要这样做，需要系里面和学校的财务帮你。可是你想想，他们这样做减少的是自己（
: 学校）的收
: 入而便宜的是你，所以politically incorrect。这是只有你一个人得利的时，没人会
: 愿意帮你的。系主任，dean知道了都不会高兴。
: 劝你不要为了这几千块去投机取巧，给自己找不必要的麻烦，不值。还是把精力放在找
: 更多的钱上吧。

c*v2019-06-20 07:06

6 楼

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

l*l2019-06-20 07:06

7 楼

关键LZ想逃掉7000块的overhead，这个学校的人会傻到帮着干么？不会吧。

C*l2019-06-20 07:06

8 楼

黎曼猜想可以试试，PNP其实最大的问题是没办法formulate question。其实人做数学
，我观察其实人做数学除了推理，枚举很重要，老邱说他为了证明卡拉比猜想，尝试了
1000多种函数，这说明计算机如果掌握了数学知识，也可以做研究。
但是人类的数学知识内容还是太丰富了，不知道怎么才能很好的输入

【在 c*******v 的大作中提到】

: Did they try the RH? P and NP?
:
: Google
: of

h*w2019-06-20 07:06

9 楼

违反规定的,不要想了.
我刚买了个一万多的程序,GRANT上走了几千刀,剩下的几千用STARTUP补上了,走两个帐,
很容易.

R*e2019-06-20 07:06

10 楼

定理机器证明已经没多大意思了，有了Tarski等人的结果，加以王浩的定理证明程序，
基本就是个小修小补的领域。

Google
of

【在 C*****l 的大作中提到】

s*t2019-06-20 07:06

11 楼

OK, 看来这个小便宜不好占。谢谢提醒。

【在 l*******l 的大作中提到】

C*l2019-06-20 07:06

12 楼

还差得远呢，机器证明本质上可以替代人类来发现新的定理。

【在 R******e 的大作中提到】

: 定理机器证明已经没多大意思了，有了Tarski等人的结果，加以王浩的定理证明程序，
: 基本就是个小修小补的领域。
:
: Google
: of

s*t2019-06-20 07:06

13 楼

老李，如果材料付学生需要跟NSF打招呼吗？还是直接付了NSF不问就不说?

【在 L***s 的大作中提到】

: 一般材料仪器不好互相转吧？
: 但是材料付学生什么的可以。NSF允许有点浮动。不过这个以后会改。

a*g2019-06-20 07:06

14 楼

有趣哦

Google
of

【在 C*****l 的大作中提到】

L*s2019-06-20 07:06

15 楼

我们office说除了付学生，别的都会有问题。不过你有点出入的话一般没人管你

【在 s**********t 的大作中提到】

: 老李，如果材料付学生需要跟NSF打招呼吗？还是直接付了NSF不问就不说?

m*r2019-06-20 07:06

16 楼

那数学系教授可以用它来写paper ? 发表？反正别人也不知道这定理是你想的，还
是机器想的。

s*t2019-06-20 07:06

17 楼

可能我也只有这样了。。。你的budget是可以买程序的吗？
看来就算不想占学校便宜省$7000，用 budget 材料的钱买小仪器也有困难啊。。

帐,

【在 h*****w 的大作中提到】

: 违反规定的,不要想了.
: 我刚买了个一万多的程序,GRANT上走了几千刀,剩下的几千用STARTUP补上了,走两个帐,
: 很容易.

m*52019-06-20 07:06

18 楼

关键是形式化，这一步很花时间

【在 R******e 的大作中提到】

: 定理机器证明已经没多大意思了，有了Tarski等人的结果，加以王浩的定理证明程序，
: 基本就是个小修小补的领域。
:
: Google
: of

s*t2019-06-20 07:06

19 楼

多谢。可能我得在NSF跟starttup之间捣腾一下。

【在 L***s 的大作中提到】

: 我们office说除了付学生，别的都会有问题。不过你有点出入的话一般没人管你

g*t2019-06-20 07:06

20 楼

有。一個例子是嚴格證明羅倫茲系統是混沌。但是作者的phd論文有bug（不是程序bug)
。後來修了另一個版本。他的phd論文我多年前看過。後來那個版本沒看。
另一個例子是開普勒裝球問題。發在annals。但是審稿人說論文是對的；不保證程序沒
bug。
這個領域很實用。等於是處理大規模電路的邏輯驗證。所以intc等公司有這專業的人。
還有半導體的tool software也有。

: 那数学系教授可以用它来写paper ? 发表？反正别人也不知道这定理是你想的
，还

: 是机器想的。

【在 m******r 的大作中提到】

: 那数学系教授可以用它来写paper ? 发表？反正别人也不知道这定理是你想的，还
: 是机器想的。

b*d2019-06-20 07:06

21 楼

只要不超过5000,问题不大.超过了5000因为有overhead问题,就不好弄了.

【在 s**********t 的大作中提到】

: 可能我也只有这样了。。。你的budget是可以买程序的吗？
: 看来就算不想占学校便宜省$7000，用 budget 材料的钱买小仪器也有困难啊。。
:
: 帐,

w*g2019-06-20 07:06

22 楼

这个方向大有可做, 就是没有funding.

bug)

【在 g****t 的大作中提到】

: 有。一個例子是嚴格證明羅倫茲系統是混沌。但是作者的phd論文有bug（不是程序bug)
: 。後來修了另一個版本。他的phd論文我多年前看過。後來那個版本沒看。
: 另一個例子是開普勒裝球問題。發在annals。但是審稿人說論文是對的；不保證程序沒
: bug。
: 這個領域很實用。等於是處理大規模電路的邏輯驗證。所以intc等公司有這專業的人。
: 還有半導體的tool software也有。
:
:
: 那数学系教授可以用它来写paper ? 发表？反正别人也不知道这定理是你想的
: ，还
:
: 是机器想的。

p*l2019-06-20 07:06

23 楼

NSF规定是salary, supply和captial之间浮动额部超过总预算的10%他们是不管的。NIH
可以浮动到25%。我们系里，一般funding agent不管他们也不说什么。我的startup
package 包了几年的工资，所以我当时把项目里的预算的工资挪去买了设备，需要给系
里会计通知一声，但是除此之外，没人管。

g*t2019-06-20 07:06

24 楼

跟集成电路设计的tool关系非常密切。过去十几年，中国08以来，至少几万亿做
集成电路。但是路线是用别人的tool，早出结果报成果。现在知道缺tool了。

【在 w***g 的大作中提到】

: 这个方向大有可做, 就是没有funding.
:
: bug)

s*t2019-06-20 07:06

25 楼

看样子只能一次不超过5000了。

【在 b*****d 的大作中提到】

: 只要不超过5000,问题不大.超过了5000因为有overhead问题,就不好弄了.

p*o2019-06-20 07:06

26 楼

没有funding就慢慢做，PDR/IC3也做了快10年了。

【在 w***g 的大作中提到】

: 这个方向大有可做, 就是没有funding.
:
: bug)

s*t2019-06-20 07:06

27 楼

多谢，请问这个百分之十的浮动在什么地方有明文提到过吗，还是不成文的规矩？我找
了一下没有找到。其实百分之十也已经相当不错了，对于一个通常的grant就有3万左右.

NIH

【在 p*l 的大作中提到】

: NSF规定是salary, supply和captial之间浮动额部超过总预算的10%他们是不管的。NIH
: 可以浮动到25%。我们系里，一般funding agent不管他们也不说什么。我的startup
: package 包了几年的工资，所以我当时把项目里的预算的工资挪去买了设备，需要给系
: 里会计通知一声，但是除此之外，没人管。

h*32019-06-20 07:06

28 楼

有哥德尔不完备定理挡前面呢

【在 C*****l 的大作中提到】

: 如果不计成本，能不能把所有数学的knowledge都输入电脑（当然是computable的形式
: ）吗？
: 。

O*r2019-06-20 07:06

29 楼

我们学校盯得最紧的就是 indirect cost，只要比预算少了，他们就会来问你。在
direct cost里换来换去他们倒是很少多嘴，当然每个 agency 有自己的规定，就像楼
上pll (娃娃鱼)讲的，Personnel and OTPS (other than personnel service) 间浮动
有规定范围。
我认识一位这样省钱：就是跟 agency要 full package postdoc (salary + max
fringe ~ 40%) 然后切割成几块招了三个 part-time student programmer，不用付
fringe。三个臭皮匠，顶个诸葛亮，最后项目也没耽搁。但即便这样学校的indirect
cost还是一个子没少。

C*l2019-06-20 07:06

30 楼

歌德尔是说任何公理体系里面都有不可判定的定理，并没有说这样的定理有多少

【在 h*********3 的大作中提到】

: 有哥德尔不完备定理挡前面呢

k*o2019-06-20 07:06

31 楼

问学校最好了。

R*e2019-06-20 07:06

32 楼

是推导出的定理，不是发现定理，就跟程序跑出结果一样，没有多少趣味。

【在 C*****l 的大作中提到】

: 还差得远呢，机器证明本质上可以替代人类来发现新的定理。

p*l2019-06-20 07:06

33 楼

我们学校规定计算机主机和显视器不算一个设备...求dell机器5000块主机最佳配置，
跑matlab并行数据处理用...

行: 我们学校盯得最紧的就是 indirect cost，只要比预算少了，他们就

【在 O*********r 的大作中提到】

: 我们学校盯得最紧的就是 indirect cost，只要比预算少了，他们就会来问你。在
: direct cost里换来换去他们倒是很少多嘴，当然每个 agency 有自己的规定，就像楼
: 上pll (娃娃鱼)讲的，Personnel and OTPS (other than personnel service) 间浮动
: 有规定范围。
: 我认识一位这样省钱：就是跟 agency要 full package postdoc (salary + max
: fringe ~ 40%) 然后切割成几块招了三个 part-time student programmer，不用付
: fringe。三个臭皮匠，顶个诸葛亮，最后项目也没耽搁。但即便这样学校的indirect
: cost还是一个子没少。

R*e2019-06-20 07:06

34 楼

为啥没房顶？就是因为行家知道不可做了。
程序的正确性证明，很容易就成为np难问题，小规模的输入还可以，集成电路那个规模
，就只好想想了。

【在 w***g 的大作中提到】

: 这个方向大有可做, 就是没有funding.
:
: bug)

M*n2019-06-20 07:06

35 楼

20K是capital purchase,
有的grant是不能买capital的。

R*e2019-06-20 07:06

36 楼

好好的不完备定理被你们说得跟笑话一样。
完备的也就是任何命题都可以判定的公理体系很多，比如欧式几何等等。
公理体系必须丰富到包含一阶皮亚诺算术，必须无矛盾或者一致，然后才有命题不可判
定。
即使可判定的公理体系也有复杂度为npc的判定问题，比如布尔逻辑范式命题的赋值问
题。

【在 C*****l 的大作中提到】

: 歌德尔是说任何公理体系里面都有不可判定的定理，并没有说这样的定理有多少

l*z2019-06-20 07:06

37 楼

想逃overhead的话可以让系里帮你建一个Fabrication,在这个fabrication下面买的
supply/equipment都可以没有overhead，但是一般的fabrication名义上是可以全校/全
系共用的（可以让其他组出recharge). 也即是说造福全校的，但实际上来说一般没人
会来用就是了。

R*e2019-06-20 07:06

38 楼

设计芯片的软件或者工具的公司有做定理机器证明的，无非就是把已有的结果用上，指
望有突破是不可能的，就是小规模的或者p复杂度的可以，其他的免谈。没有，不可以
，有也不指望有多大作用。

s*t2019-06-20 07:06

39 楼

一个postdoc换三学生，这个是个好deal。这个indirect cost 还真是他们买米下锅的
钱。。。。

【在 O*********r 的大作中提到】

R*e2019-06-20 07:06

40 楼

Tarski的结果和Grobner等人的算法经常就是指数级别的，大多数时候就是看看而已。
这个领域的人，缺了不行，大用也是浪费。就这现状，大家归安吧。

s*t2019-06-20 07:06

41 楼

想问他们之前有点准备。。。看样子很难。

【在 k****o 的大作中提到】

: 问学校最好了。

C*l2019-06-20 07:06

42 楼

本质上没有不可逾越的鸿沟，定理要证明了才能叫定理，如果电脑可以证明或者证伪大
量给定定理，就可以让电脑生成新定理，再去证明。

【在 R******e 的大作中提到】

: 是推导出的定理，不是发现定理，就跟程序跑出结果一样，没有多少趣味。

s*t2019-06-20 07:06

43 楼

这个建议的确好！！！
我有些仪器本系跟外系的同事都需要用，有人也问过怎么付账。因为他们用的不多所以我
都说算了。这样说来真要考虑一下了。
希望你说的在这个fabrication下面买的supply/equipment都可以没有overhead不是你
们学校的特例。

【在 l**z 的大作中提到】

: 想逃overhead的话可以让系里帮你建一个Fabrication,在这个fabrication下面买的
: supply/equipment都可以没有overhead，但是一般的fabrication名义上是可以全校/全
: 系共用的（可以让其他组出recharge). 也即是说造福全校的，但实际上来说一般没人
: 会来用就是了。

C*l2019-06-20 07:06

44 楼

行家根本不作数，搞神经网络那几位几十年就靠几十万的小funding勉强维持，最后还
是那些重金投入的方向被这个方向打败

【在 R******e 的大作中提到】

: 为啥没房顶？就是因为行家知道不可做了。
: 程序的正确性证明，很容易就成为np难问题，小规模的输入还可以，集成电路那个规模
: ，就只好想想了。

a*y2019-06-20 07:06

45 楼

这个算不算bait and switch, agency不管么? category也不对吧

【在 O*********r 的大作中提到】

x*u2019-06-20 07:06

46 楼

因为tool可以盗版，不怕国外封锁

【在 g****t 的大作中提到】

: 跟集成电路设计的tool关系非常密切。过去十几年，中国08以来，至少几万亿做
: 集成电路。但是路线是用别人的tool，早出结果报成果。现在知道缺tool了。

A*02019-06-20 07:06

47 楼

对公立学校来说，一个postdoc换三学生，是个好deal，因为学生学费低。
对私立学校，三个学生的学费可是很大的一笔开销。

【在 s**********t 的大作中提到】

: 一个postdoc换三学生，这个是个好deal。这个indirect cost 还真是他们买米下锅的
: 钱。。。。

R*e2019-06-20 07:06

48 楼

读读开辟新领域的定理的证明就知道了，那不是计算机能证明的。
依照Godel定理，必须添加新公理，才能有有趣味的定理产生出来，否则就是跑程序而
已。
数学不该看作定理的证明，它是靠人的直觉和准形式化的方法构建的真命题的集合。

【在 C*****l 的大作中提到】

: 本质上没有不可逾越的鸿沟，定理要证明了才能叫定理，如果电脑可以证明或者证伪大
: 量给定定理，就可以让电脑生成新定理，再去证明。

A*02019-06-20 07:06

49 楼

DELL WS T5500/T5600
评测
http://www.cgchannel.com/2012/12/review-dell-precision-t5600-wo
老款5500
http://www.amazon.com/gp/product/B00EYIRP52/ref=as_li_qf_sp_asi
新款5600
http://configure.us.dell.com/dellstore/config.aspx?oc=swct564&m

【在 p*l 的大作中提到】

: 我们学校规定计算机主机和显视器不算一个设备...求dell机器5000块主机最佳配置，
: 跑matlab并行数据处理用...
:
: 行: 我们学校盯得最紧的就是 indirect cost，只要比预算少了，他们就

R*e2019-06-20 07:06

50 楼

如常用于定理机器证明的Buchberger's algorithm,其算法是指数复杂度的。
https://en.wikipedia.org/wiki/Buchberger%27s_algorithm
还有Tarski的结果，其算法也至少是指数复杂度的：
https://en.wikipedia.org/wiki/Tarski%E2%80%93Seidenberg_theorem。
不服来辩。哇哈哇哈

b*d2019-06-20 07:06

51 楼

Definitely a red flag for audit.
U don't have a budget for equipment. Any charged on equip category will
trigger attention at sponsored program. They won't allow u to do that.
Except NSF pm allowed u to do a rebudget.

【在 s**********t 的大作中提到】

: 现在手上有一个NSF的3年的grant，每年materials/supplies 的budget大概是$7000左
: 右，第一年我就老老实实的吧这$7000钱买材料了。现在还剩$14,000，算上overhead的
: 话大概还有$21,000左右。现在项目进行到一半需要买一个小的仪器，大概$20,000。我
: 想问的是我能不能够用这个本来买materials/supplies的钱去买这个小仪器。如果可以
: 的话就相当于节约了我$7000 的 overhead，然后我用我自己的startup的钱买
: materials/supplies就行了，反正startup的钱没有overhead.
: 1.这样做的话学校会不会不高兴，因为他们就少了$7000 的 overhead赚。
: 2.对NSF来说他们会在乎吗？反正我会继续用我的startup的钱买materials/supplies。
: 每年report时候他们会检查钱到底花在什么地方了吗？我需不需要要写一个
: justification来说明这样做确实有利于这个项目？在我看来这个确实是好事啊，唯一

C*l2019-06-20 07:06

52 楼

直觉是靠不住的，给人类神秘的虚荣感觉，就好比以前围棋高手也说是靠直觉，其实就
是一种计算而已。一个简单的类比，一个数学定理可不可以通过自然语言解释给别人听
，当然是可以得。既然是可以得，为啥不能建立基于自然语言的计算？

【在 R******e 的大作中提到】

: 读读开辟新领域的定理的证明就知道了，那不是计算机能证明的。
: 依照Godel定理，必须添加新公理，才能有有趣味的定理产生出来，否则就是跑程序而
: 已。
: 数学不该看作定理的证明，它是靠人的直觉和准形式化的方法构建的真命题的集合。

s*t2019-06-20 07:06

53 楼

that sounds scary....
I was hopping to do this in secret but looks it will never fly...

【在 b*****d 的大作中提到】

: Definitely a red flag for audit.
: U don't have a budget for equipment. Any charged on equip category will
: trigger attention at sponsored program. They won't allow u to do that.
: Except NSF pm allowed u to do a rebudget.

R*e2019-06-20 07:06

54 楼

不用这么辩解，拿个实例来吧：比如从欧几里德几何到非欧几何，这个应该是计算机做
不到的，怎么证明第五公设是独立的？
复几何和理想、素数之间的关系咋找出来？
再随便举个例子：一般意义上的发散级数可启发不同可和性的定义，你让计算机做？
看看数学史，每一次大定理的证明，都不是靠形式化能解决的，都有直觉。

【在 C*****l 的大作中提到】

: 直觉是靠不住的，给人类神秘的虚荣感觉，就好比以前围棋高手也说是靠直觉，其实就
: 是一种计算而已。一个简单的类比，一个数学定理可不可以通过自然语言解释给别人听
: ，当然是可以得。既然是可以得，为啥不能建立基于自然语言的计算？

b*d2019-06-20 07:06

55 楼

天啊. 你胆太大了.osp post award 每天的工作就是monitor fund activity.你想想
financial report 上 budget expenses..你0 budget 的category, 突然出现个5k. 变
负, postawrad administrator 马上就收到警告了。你到是可以跟系里协调个可行的
办法
不信你可以试试.我怀疑你order 都下不了.因为你那category 没钱学校采购系统会自
动return 说 insufficient funding.

【在 s**********t 的大作中提到】

: that sounds scary....
: I was hopping to do this in secret but looks it will never fly...

R*e2019-06-20 07:06

56 楼

恰巧RH不好形式化，而P=NP形式化得差不多了。我纳闷你们形式化的定义是啥。

【在 C*****l 的大作中提到】

: 黎曼猜想可以试试，PNP其实最大的问题是没办法formulate question。其实人做数学
: ，我观察其实人做数学除了推理，枚举很重要，老邱说他为了证明卡拉比猜想，尝试了
: 1000多种函数，这说明计算机如果掌握了数学知识，也可以做研究。
: 但是人类的数学知识内容还是太丰富了，不知道怎么才能很好的输入

b*d2019-06-20 07:06

57 楼

secret肯定是不行的。因为是从不同的line里出来的。

【在 s**********t 的大作中提到】

: that sounds scary....
: I was hopping to do this in secret but looks it will never fly...

R*e2019-06-20 07:06

58 楼

反推数学就是reverse math基本就是探索哪部分数学需要多强的公理体系，事实上全部
现代数学不可能递归公理化，这已经是常识。
再说一遍，全部数学不等同证明定理

【在 h*********3 的大作中提到】

: 有哥德尔不完备定理挡前面呢

b*d2019-06-20 07:06

59 楼

有的agent是允许在学生和postdoc之间switch的。这个也是要osp的人帮你从不同的
line里挪钱。

【在 a**********y 的大作中提到】

: 这个算不算bait and switch, agency不管么? category也不对吧

R*e2019-06-20 07:06

60 楼

弄明白这两个方向的基本知识就知道两者不可比。

【在 C*****l 的大作中提到】

: 行家根本不作数，搞神经网络那几位几十年就靠几十万的小funding勉强维持，最后还
: 是那些重金投入的方向被这个方向打败

b*d2019-06-20 07:06

61 楼

那是因为这都是personnel cost 算一个总的category. 像equip 和supply 不是一个
category

【在 b*****d 的大作中提到】

: 有的agent是允许在学生和postdoc之间switch的。这个也是要osp的人帮你从不同的
: line里挪钱。

x*u2019-06-20 07:06

62 楼

阿法狗也是直觉
机器现在只有直觉，逻辑推理还得靠传统方法

【在 C*****l 的大作中提到】

L*s2019-06-20 07:06

63 楼

不会的。大多数时候都会允许你下单。因为你开始的项目分布和具体的其实有很大区别
。但是如果太离谱，比如材料变设备，就会有人问。

【在 b*****d 的大作中提到】

: 天啊. 你胆太大了.osp post award 每天的工作就是monitor fund activity.你想想
: financial report 上 budget expenses..你0 budget 的category, 突然出现个5k. 变
: 负, postawrad administrator 马上就收到警告了。你到是可以跟系里协调个可行的
: 办法
: 不信你可以试试.我怀疑你order 都下不了.因为你那category 没钱学校采购系统会自
: 动return 说 insufficient funding.

C*l2019-06-20 07:06

64 楼

阿法狗不是仅仅靠直觉，神经网络是直觉，但是模特卡罗树搜索是很严谨的求证过程。

【在 x****u 的大作中提到】

: 阿法狗也是直觉
: 机器现在只有直觉，逻辑推理还得靠传统方法

b*d2019-06-20 07:06

65 楼

那是你们学校比较宽松。我们学校grant 某人category一没有钱马上return
requisition.要求你别的账户先垫付

【在 L***s 的大作中提到】

: 不会的。大多数时候都会允许你下单。因为你开始的项目分布和具体的其实有很大区别
: 。但是如果太离谱，比如材料变设备，就会有人问。

C*l2019-06-20 07:06

66 楼

不要这么狭窄地看待计算机，如果人类可以基于联想，类比，扩展发现新的理论，电脑
本质上也可以。问题是现在表征问题的方法比较死板，自然语言其实这个时候更厉害。

【在 R******e 的大作中提到】

: 不用这么辩解，拿个实例来吧：比如从欧几里德几何到非欧几何，这个应该是计算机做
: 不到的，怎么证明第五公设是独立的？
: 复几何和理想、素数之间的关系咋找出来？
: 再随便举个例子：一般意义上的发散级数可启发不同可和性的定义，你让计算机做？
: 看看数学史，每一次大定理的证明，都不是靠形式化能解决的，都有直觉。

L*s2019-06-20 07:06

67 楼

这个太夸张了...

【在 b*****d 的大作中提到】

: 那是你们学校比较宽松。我们学校grant 某人category一没有钱马上return
: requisition.要求你别的账户先垫付

R*e2019-06-20 07:06

68 楼

原来你是做哲学的，我输了。

【在 C*****l 的大作中提到】

: 不要这么狭窄地看待计算机，如果人类可以基于联想，类比，扩展发现新的理论，电脑
: 本质上也可以。问题是现在表征问题的方法比较死板，自然语言其实这个时候更厉害。

p*l2019-06-20 07:06

69 楼

如果你本来NSF的budget没有capital，确实是很难用这个钱去买capital。我读博士的
时候，有一次居然连开会的钱都没法报，因为老板的NSF做budget忘了写travel，后来
老板找学校改了budget才报掉。如果budget原来就有capital，相对容易一点，比如说
我的grant上travel的钱，总是超预算。到现在为止，我还没碰到有人问过。

【在 s**********t 的大作中提到】

: that sounds scary....
: I was hopping to do this in secret but looks it will never fly...

x*u2019-06-20 07:06

70 楼

蒙特卡洛树一直就有，阿法狗的突破时机器直觉

【在 C*****l 的大作中提到】

: 阿法狗不是仅仅靠直觉，神经网络是直觉，但是模特卡罗树搜索是很严谨的求证过程。

l*12019-06-20 07:06

71 楼

LZ can tty to get funding from 1000 talent short term from CN side...

c*v2019-06-20 07:06

72 楼

有个文章讲RH可以等价成一个只用非常简单的逻辑的不等式来进行验证。
我以前写过程序。非常慢。远不如现有的siegel／图灵／黎曼算法。
但是这证明了RH可以简化为一个非常简单的计算机程序的停机问题。
也就是可以形式化。

【在 R******e 的大作中提到】

: 恰巧RH不好形式化，而P=NP形式化得差不多了。我纳闷你们形式化的定义是啥。

R*e2019-06-20 07:06

73 楼

你说的是王浩《数理逻辑通俗讲话》里关于RH的那个命题吧？那是一个穷举，如果RH成
立，就会一路跑下去，永远不停机。没意义的。那不叫数学证明，只能叫数值计算或者
数值验证。
定理的机器证明步骤应该是finite的，尽管是指数级别甚至是更高。

【在 c*******v 的大作中提到】

: 有个文章讲RH可以等价成一个只用非常简单的逻辑的不等式来进行验证。
: 我以前写过程序。非常慢。远不如现有的siegel／图灵／黎曼算法。
: 但是这证明了RH可以简化为一个非常简单的计算机程序的停机问题。
: 也就是可以形式化。

c*v2019-06-20 07:06

74 楼

没人讲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*v2019-06-20 07:06

75 楼

多年前在国内,看到普渡有个教授，公布自己证明了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*e2019-06-20 07:06

76 楼

还没看，如果是RH的机器证明程序，错的概率极高。

【在 c*******v 的大作中提到】

R*e2019-06-20 07:06

77 楼

服了你了，有复数未必就复杂。
你的低阶逻辑能低到多少？
你逗人玩。
那文章跟定理的机器证明或RH的形式化没有丝毫关系，咣当！

【在 c*******v 的大作中提到】

c*v2019-06-20 07:06

78 楼

这种逻辑复杂程度的刻画叫做"Pi one sentence".
历史上有人做过的。
RH本身是严格的数学猜想，怎么会有形式化问题。
有问题的是可以简化到只用哪几个符号。
最后你查一下我几年前写的literature programming的一点notes。我看一个问题
一般至少到那个程度的细节。在我了解的细节知识以下的道听途说，不回复了。

【在 R******e 的大作中提到】

: 服了你了，有复数未必就复杂。
: 你的低阶逻辑能低到多少？
: 你逗人玩。
: 那文章跟定理的机器证明或RH的形式化没有丝毫关系，咣当！

R*e2019-06-20 07:06

79 楼

受不了了。
依照数的扩张，得从皮亚诺公理一路到复数，你先试试。即使用非标准模型，你也得
定义出素数，积分，开拓等等吧。你先试试咋形式化这些。
至于表述为一个命题，这是个trivial的工作，只看长短而已，看来你现在不熟悉math
logic的基本知识了。
真没兴趣多说了，版上不少哲学家。

【在 c*******v 的大作中提到】

: 这种逻辑复杂程度的刻画叫做"Pi one sentence".
: 历史上有人做过的。
: RH本身是严格的数学猜想，怎么会有形式化问题。
: 有问题的是可以简化到只用哪几个符号。
: 最后你查一下我几年前写的literature programming的一点notes。我看一个问题
: 一般至少到那个程度的细节。在我了解的细节知识以下的道听途说，不回复了。

C*l2019-06-20 07:06

80 楼

难不代表不可能，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*t2019-06-20 07:06

81 楼

RH跟初等数论不等式等价。你是不是看不懂英语文章？这是两个文章证明过的。
我有本数论书，偶尔还刷着题呢。

math

【在 R******e 的大作中提到】

R*e2019-06-20 07:06

82 楼

俺没看懂，俺看到文章跟机器证明或者形式化毫无关系。再摆出十个跟RH等价的初等数
学命题，也跟形式化没关系。
难道我说错了吗？
算了，给你的建议就是，你就当作爱好玩玩吧，现代数论你基本弄不懂多少，比如丢番
图几何或称算术代数几何，代数几何都看得费劲，咋弄算术代数几何？

【在 g****t 的大作中提到】

: RH跟初等数论不等式等价。你是不是看不懂英语文章？这是两个文章证明过的。
: 我有本数论书，偶尔还刷着题呢。
:
: math

c*v2019-06-20 07:06

83 楼

初等数论不等式本身就是严格形式化的。在皮亚诺算术之内。
RH的形式化问题，你指的是什么意思？

【在 R******e 的大作中提到】

: 俺没看懂，俺看到文章跟机器证明或者形式化毫无关系。再摆出十个跟RH等价的初等数
: 学命题，也跟形式化没关系。
: 难道我说错了吗？
: 算了，给你的建议就是，你就当作爱好玩玩吧，现代数论你基本弄不懂多少，比如丢番
: 图几何或称算术代数几何，代数几何都看得费劲，咋弄算术代数几何？

R*e2019-06-20 07:06

84 楼

一阶皮亚诺算术是严格形式化的，二阶的你见过几个形式化的。不过很多人分不清一阶
和二阶，出错不足为怪。我没兴趣解释基本概念。
话说，你不是不回复了吗？

【在 c*******v 的大作中提到】

: 初等数论不等式本身就是严格形式化的。在皮亚诺算术之内。
: RH的形式化问题，你指的是什么意思？

c*v2019-06-20 07:06

85 楼

RH在PA之内是证明过的数学定理。看我给的引文你就知道了。
这回真不再继续跟你解释了。

【在 R******e 的大作中提到】