还AI拥有顶级数学家能力？？我给它5条公理，它能无中生有的 把所有平面几何定理推导出来吗？

[Jack12345]

还AI拥有顶级数学家能力？？我给它平面几何5条公理，它能无中生有的 把所有平面几何定理推导出来吗？

关键是要 无中生有？已经训练好的不算。或者 AI 理解了什么是 那5条公理吗？

或者反过来，我给它 一大堆平面几何图形，它能自己提炼出 那5条公理吗 ？

就是一个在人类现有知识范围内的 内插值，一个应用统计工具，吹得跟什么似的

[cocoa]

5条不夠。严格来說，人也不能从5条推出所有歐氏几何定理。但人能糊弄。

[Jack12345]

5条不夠。严格来說，人也不能从5条推出所有歐氏几何定理。但人能糊弄。

哪条歐氏几何定理 不能从5条公理推出来的？举个例子

[cocoa]

哪条歐氏几何定理 不能从5条公理推出来的？举个例子

大多數吧，說起來就长了。你只是以為你能推出来，其實中間都有gap。

[shanghaibaba]

还AI拥有顶级数学家能力？？我给它平面几何5条公理，它能无中生有的 把所有平面几何定理推导出来吗？

关键是要 无中生有？已经训练好的不算。或者 AI 理解了什么是 那5条公理吗？

或者反过来，我给它 一大堆平面几何图形，它能自己推导出 那5条公理吗 ？

就是一个在人类现有知识范围内的 内插值，一个应用统计工具，吹得跟什么似的

你这个说的是有道理的。所谓ai证明数学定理只不过是有数学家帮它定好了方向让它去一个非常局限的小区域内进行推演而已，本质上就是个逻辑计算器，理论上不比以前用Mathematica推公式更高级。

[forecasting]

还AI拥有顶级数学家能力？？我给它平面几何5条公理，它能无中生有的 把所有平面几何定理推导出来吗？

关键是要 无中生有？已经训练好的不算。或者 AI 理解了什么是 那5条公理吗？

或者反过来，我给它 一大堆平面几何图形，它能自己推导出 那5条公理吗 ？

就是一个在人类现有知识范围内的 内插值，一个应用统计工具，吹得跟什么似的

这在五六十年代就实现了，还要现在的LLM做？

[shanghaibaba]

这在五六十年代就实现了，还要现在的LLM做？

晕呀，哪个ai能够自行提取出几何公里？

[forecasting]

晕呀，哪个ai能够自行提取出几何公里？

Tarski实闭域判定算法（Real Closed Fields, RCF）的应用之一就是证明欧式几何的所有定理。

Tarski 实闭域的判定算法，本质上就是一阶实数理论（First-order Theory of Real Closed Fields）的量词消去（Quantifier Elimination）。它的复杂度经历了几十年的改进。
事实上，RCF 因为具有量词消去和 o-minimal 结构，其可定义集合始终是半代数集，这也是其复杂度与 Presburger 算术、代数闭域判定之间形成明显对比的原因。

平面几何的情况有中科院院士张景中做的系统，理论意义几乎没意义，但可用于教育，可没推广开。

吴文俊那套算法跟Tarski差不多，所以理论意义也不大

@TheMatrix 多奖赏一些分，我难得愿意写这么多，而且质量不错 @verdelite

[forecasting]

Tarski实闭域判定算法（Real Closed Fields, RCF）的应用之一就是证明欧式几何的所有定理。

Tarski 实闭域的判定算法，本质上就是一阶实数理论（First-order Theory of Real Closed Fields）的量词消去（Quantifier Elimination）。它的复杂度经历了几十年的改进。
事实上，RCF 因为具有量词消去和 o-minimal 结构，其可定义集合始终是半代数集，这也是其复杂度与 Presburger 算术、代数闭域判定之间形成明显对比的原因。

平面几何的情况有中科院院士张景中做的系统，理论意义几乎没意义，但可用于教育，可没推广开。

吴文俊那套算法跟Tarski差不多，所以理论意义也不大

这里提到 o-minimal 结构，正是北大谢俊逸缺的那一部分知识和训练之一小部分。

@Caravel

很不幸，谢在中国没接触到，跑法国，法国也不重视这一部分

[forecasting]

非要求自动输出定理机器证明，不过就是在Tarski算法上加几行代码的事。

[Jack12345]

Tarski实闭域判定算法（Real Closed Fields, RCF）的应用之一就是证明欧式几何的所有定理。

Tarski 实闭域的判定算法，本质上就是一阶实数理论（First-order Theory of Real Closed Fields）的量词消去（Quantifier Elimination）。它的复杂度经历了几十年的改进。
事实上，RCF 因为具有量词消去和 o-minimal 结构，其可定义集合始终是半代数集，这也是其复杂度与 Presburger 算术、代数闭域判定之间形成明显对比的原因。

平面几何的情况有中科院院士张景中做的系统，理论意义几乎没意义，但可用于教育，可没推广开。

吴文俊那套算法跟Tarski差不多，所以理论意义也不大

@TheMatrix 多奖赏一些分，我难得愿意写这么多，而且质量不错 @verdelite

第1，我没有听说过 用 Tarski实闭域判定算法（Real Closed Fields, RCF）能够来证明欧式几何的所有定理，也很少听到有科普 来说明这个方面的工作，也没有造成轰动新闻。所以我对大家是否公认 Tarski 算法能够证明欧式几何的所有定理 表示很大的怀疑。还是只是那帮人的自吹自擂 自我claim ？

第2，退一万步来说，就算Tarski实闭域判定算法 能够证明欧式几何的所有定理，早在上世纪 60年代 就提出来了。那也是人类想出来的算法，计算机只是运行执行一下而已，也不是计算机提出来的。和冒泡排序法 或四色问题 一个模样

所以 所谓的AI本身 还是没有能够自己想出来办法 来证明平面几何的定理

[cocoa]

第1，我没有听说过 用 Tarski实闭域判定算法（Real Closed Fields, RCF）能够来证明欧式几何的所有定理，也很少听到有科普 来说明这个方面的工作，也没有造成轰动新闻。所以我对大家是否公认 Tarski 算法能够证明欧式几何的所有定理 表示很大的怀疑。还是只是那帮人的自吹自擂 自我claim ？

第2，退一万步来说，就算Tarski实闭域判定算法 能够证明欧式几何的所有定理，早在上世纪 60年代 就提出来了。那也是人类想出来的算法，计算机只是运行执行一下而已，也不是计算机提出来的。和冒泡排序法 或四色问题 一个模样

所以 所谓的AI本身 还是没有能够自己想出来办法 来证明平面几何的定理

我也不喜歡這类算法。我以為這不是一个体系的東西，硬說證出來了也不好反駁，但总不是那個味。一般認為数學是严格的，但其實远远达不到哲学要求的严格。你的問題其實不該是AI能不能證（什麼算證標准其實依賴人的直覺）所有定理，而是Al能不能提取符合人类直觉的附加公理完善原有五条公理。

[shot]

还AI拥有顶级数学家能力？？我给它平面几何5条公理，它能无中生有的 把所有平面几何定理推导出来吗？

关键是要 无中生有？已经训练好的不算。或者 AI 理解了什么是 那5条公理吗？

或者反过来，我给它 一大堆平面几何图形，它能自己推导出 那5条公理吗 ？

就是一个在人类现有知识范围内的 内插值，一个应用统计工具，吹得跟什么似的

你说的这些，AI早就能做过了。提出公理，并建立体系，这个事情对AI来说不难。
你说的这些，你自己反而做不到。做到的是欧几里得，不是你。

[Jack12345]

你说的这些，AI早就能做过了。提出公理，并建立体系，这个事情对AI来说不难。
你说的这些，你自己反而做不到。做到的是欧几里得，不是你。

呵呵，AI 做到了？给出例子

[forecasting]

第1，我没有听说过 用 Tarski实闭域判定算法（Real Closed Fields, RCF）能够来证明欧式几何的所有定理，也很少听到有科普 来说明这个方面的工作，也没有造成轰动新闻。所以我对大家是否公认 Tarski 算法能够证明欧式几何的所有定理 表示很大的怀疑。还是只是那帮人的自吹自擂 自我claim ？

第2，退一万步来说，就算Tarski实闭域判定算法 能够证明欧式几何的所有定理，早在上世纪 60年代 就提出来了。那也是人类想出来的算法，计算机只是运行执行一下而已，也不是计算机提出来的。和冒泡排序法 或四色问题 一个模样

所以 所谓的AI本身 还是没有能够自己想出来办法 来证明平面几何的定理

你一外行，没听说过正常

[Jack12345]

你一外行，没听说过正常

呵呵，你们那个小圈子 孤芳自赏 自吹自擂去吧。

出了你们那个小圈子，没人承认 那个所谓的Tarski实闭域判定算法 能够证明欧式几何的所有定理。没有公认的共识

[forecasting]

呵呵，你们那个小圈子 孤芳自赏 自吹自擂去吧。

出了你们那个小圈子，没人承认 那个所谓的Tarski实闭域判定算法 能够证明欧式几何的所有定理。没有公认的共识

你啥都不懂，有啥资格说小圈子？你学啥的，敢来谈AI和Tarski算法？

[Jack12345]

你啥都不懂，有啥资格说小圈子？你学啥的，敢来谈AI和Tarski算法？

讲不过了 就开始质疑别人啥也不懂了。呵呵

我现在 工作上就是搞 AI 的，一天到晚在弄 pyTorch 的，不能谈论了 ？

[forecasting]

讲不过了 就开始质疑别人啥也不懂了。呵呵

我现在 工作上就是搞 AI 的，一天到晚在弄 pyTorch 的，不能谈论了 ？

那你真是个外行，连计算机理论的abc都不懂，半路出家，还是哪个烂校毕业的？

[Jack12345]

那你真是个外行，连计算机理论的abc都不懂，半路出家，还是哪个烂校毕业的？

呵呵，你别来质疑我的资格了。你还不够格

你要真有空 就来科普一下 这个所谓的 Tarski实闭域判定算法（Real Closed Fields, RCF）吧，看能不能把大家说服