x****u
发帖数: 44466 | |
l**o
发帖数: 131 | 2 LOL, 可以倒过来，把四色定理出到IMO里面去？吴文俊搞的那些初等几何机器证明的东
西，俺不懂，不过能不能搞出几个难点的定理，也出到IMO里面去？ |
C*****l
发帖数: 1 | 3 瞎搞，小学考题都做不了
【在 x****u 的大作中提到】
: https://imo-grand-challenge.github.io/
: 目标是计算机拿奥数金牌
|
x****u
发帖数: 44466 | 4 这个东西目前只是个想法
首先msr需要搞定数学证明的形式化表示，他们那个lean语言也是开发中
【在 l**o 的大作中提到】
: LOL, 可以倒过来，把四色定理出到IMO里面去？吴文俊搞的那些初等几何机器证明的东
: 西，俺不懂，不过能不能搞出几个难点的定理，也出到IMO里面去？
|
x****u
发帖数: 44466 | 5 日本人已经做了高考AI，虽然考不上预定目标的东大，但是能考上中等偏上大学了
【在 C*****l 的大作中提到】
: 瞎搞，小学考题都做不了
|
C*****l
发帖数: 1 | 6 细节从来没有人敢透露，如果能从读自然语言的卷子开始做，能做一道大题出来我就信。
【在 x****u 的大作中提到】
: 日本人已经做了高考AI，虽然考不上预定目标的东大，但是能考上中等偏上大学了
|
f******2
发帖数: 2455 | 7 能给个链接吗？谢谢！
: 日本人已经做了高考AI，虽然考不上预定目标的东大，但是能考上中等偏
上大学了
【在 x****u 的大作中提到】
: 日本人已经做了高考AI，虽然考不上预定目标的东大，但是能考上中等偏上大学了
|
x****u
发帖数: 44466 | 8 https://ja.wikipedia.org/wiki/%E6%9D%B1%E3%83%AD%E3%83%9C%E3%81%8F%E3%82%93
【在 f******2 的大作中提到】
: 能给个链接吗？谢谢！
:
:
: 日本人已经做了高考AI，虽然考不上预定目标的东大，但是能考上中等偏
: 上大学了
:
|
C*****l
发帖数: 1 | 9 最多做点知识问答和写作，其他的都是鬼扯。
真要能做IMO题了，那和数学家还能差多少? 当然我说的是从自然语言和图像识别开始
，如果是有人把他转成等效的程序输入，那就是类似机器证明一类的东西了
93
【在 x****u 的大作中提到】
: https://ja.wikipedia.org/wiki/%E6%9D%B1%E3%83%AD%E3%83%9C%E3%81%8F%E3%82%93
|
x****u
发帖数: 44466 | 10 你知不知道机器证明的发展也早就停滞了，证明不了IMO级别的问题。
【在 C*****l 的大作中提到】
: 最多做点知识问答和写作，其他的都是鬼扯。
: 真要能做IMO题了，那和数学家还能差多少? 当然我说的是从自然语言和图像识别开始
: ，如果是有人把他转成等效的程序输入，那就是类似机器证明一类的东西了
:
: 93
|
|
|
x****u
发帖数: 44466 | 11 你仔细看下介绍再说吧
【在 C*****l 的大作中提到】
: 最多做点知识问答和写作，其他的都是鬼扯。
: 真要能做IMO题了，那和数学家还能差多少? 当然我说的是从自然语言和图像识别开始
: ，如果是有人把他转成等效的程序输入，那就是类似机器证明一类的东西了
:
: 93
|
C*****l
发帖数: 1 | 12 那是日文得，我看不明白
【在 x****u 的大作中提到】
: 你仔细看下介绍再说吧
|
C*****l
发帖数: 1 | 13 机器不是证明过4色定理么
【在 x****u 的大作中提到】
: 你知不知道机器证明的发展也早就停滞了，证明不了IMO级别的问题。
|
x****u
发帖数: 44466 | 14 就是我说的意思
考上东大当然要用日语啊。。。
【在 C*****l 的大作中提到】
: 那是日文得，我看不明白
|
x****u
发帖数: 44466 | 15 两回事
机器还能用暴力搜索证明证否很多人力做不到的事情，不等于其能搞定IMO
【在 C*****l 的大作中提到】
: 机器不是证明过4色定理么
|
