哥德巴赫猜想 [HOT]

弄了半天 #CoolApk 那个『著名』的撕逼热点功能居然是从 #ZhiHU 抄过来的啊...

#TeX #Math #ZhiHu #Share 已经完成排版，感谢知乎用户之前的排版。我只修改了一些无关紧要的语言描述和文档排版，证明逻辑完全没有碰，大家可以随便找茬子

渲染结果在这里，适合没有 XeLaTeX 环境的鉴赏（

我对这玩意的评价：除了可以拿来练习数学使用基本数论的公式模式识别外，没有啥卵用

如果排版得不好，不好看，你们会不明觉厉（比如看王淫博客上那些 Scheme 代码、forall 类型、intersection 类型表示什么的）

｛看不懂就觉得很厉害，当然啦，不是所有人都学过 Scala 写过 Clojure，很多产业界的（当然对于现在很多小应用开发者我觉得都不能算作工业界的开发人员）程序员都只写过 imperative （表述式）语言｝

只要我们稍微排版得好看一点，再加上自己有点公式识别的能力，我相信你会发现都是很简单的逻辑和关系，相当基础，就差是高三水平了。基本不涉及多高等的数学

然后 TeX 随便写点代码排个版，博客写点 MathJax，还不用到为 TeX 编程（写扩展包啊...）的级别，就是很多人所谓的大佬，其实这点技能又有什么，说到底还是自己菜了（说真的）

(其实对于一般 TeX 排版系统的用途也就和 HTML 渲染引擎的用途一样的，没什么大不了的... 但有些人不想了解就会... 呃... 文体两开花？（跑））

但我觉得非常无聊，至于对此证明的错误知乎上当然讨论，不如去看看？

对啦，我之前还有一个简单的非常非常 trivial 的定理证明学习中我自己因为智商原因踩到的坑，所以写了笔记，要不要看一下

高中生对哥德巴赫猜想的证明有哪些错误？ - 陈沉沉的回答 - 知乎
https://www.zhihu.com/question/307595822/answer/563758084

阅读笔记 #Proof #Math

== 为什么逆反命题正确？

结论为真，不管假设如何，命题恒为真。

没有例子光给定义我不习惯，所以不讲。
概念太抽象了，况且我又没有得到多少逻辑学上的形式化定义，或者说我不需要形式化定义，但至少我得清楚概念啊？
不怕你们说我笨，骄傲点说，比我笨的人多了，显然我是闲的没事才会弄这些。

== 逻辑漏洞在哪里？

假设为假，命题恒为真，结论不一定为真。

例如：美女对舔狗说：男人都死绝了，我会嫁给你。
  该命题为真，但不能说美女嫁给舔狗是对的。

这个命题就是说 所有男人都死了 → 美女会嫁给添狗
或者说命题 所有男人都死了 成立『蕴含』 美女会嫁给添狗成立

这个命题的假设是 所有男人都死光了



美女对舔狗说

表明了至少此命题（所有男人都死了 → 美女会嫁给添狗）这个复合命题是的确成立的（恒为真）
但是不能不考虑前提条件（假设）所有男人都死光了，我们知道在这里它不成立，所以无法通过（所有男人都死了 → 美女会嫁给添狗）这个既成条件得出结论『美女会嫁给添狗』

『我也是刚刚注意到 (p -> q) 是一个单独的命题... 描述的是『由命题 p 成立可以推导出命题 q 成立』这个命题（p 『蕴含』 q）

命题 (p -> r) -> (q -> r) -> (p ∨ q -> r) 不一定要求 p 和 q 都成立才成立... 可惜我现在才看得懂』

== 所以到底错误在哪里？

回到原证明。如果把-1定义成质数，那么逆反命题不为真，证明错。如果把-1不定义成质数，那么假设为假，不能说明结论为真。

懒得理解了... 反正就是说不管 -1 是否被定义为质数这个确定性问题是否为真，证明都不成立
如果 -1 的确被定义为质数，则命题的逆反命题不为真，无法得证
如果 -1 没有被定义为质数，则命题的假设不成立，同样无法得证

== 此知乎问题的原答案

猜想：如果我妈是男的，那么哥德巴赫猜想成立，黎曼猜想成立，P=NP。

证明：如果哥德巴赫猜想不成立，黎曼猜想不成立，P≠NP，那么我妈是女的。

这个逆反命题显然正确。那么证明题也正确。恭喜我证明出来哥德巴赫猜想，黎曼猜想以及P=NP。

在这里，命题『猜想』即为 （

我妈是男的

→

哥德巴赫猜想成立

→

黎曼猜想成立

→

P=NP

）
它是成立的，这是我们证明的既成条件

而作者的证明（错误的）是 （

哥德巴赫猜想不成立

→

黎曼猜想成立

→

P≠NP

→

我妈是女的

）
它是成立的，但我们最终要证明的其实是

哥德巴赫猜想成立

而作者的错误在于他说因为我妈是女的，所以

哥德巴赫猜想成立

，或者说复合命题

（

我妈是男的

→

哥德巴赫猜想成立

→

黎曼猜想成立

→

P=NP

） →
（

哥德巴赫猜想不成立

→

黎曼猜想成立

→

P≠NP

→

我妈是女的

） →

我妈是女的

→ 哥德巴赫猜想成立 成立

这里『我妈』非男即女，

哥德巴赫猜想不成立

是说 ¬(Logical NOT)

哥德巴赫猜想成立

明显就是谬误，建议先去 wikipedia 好好恶补一下数学证明。

在这里，『这个命题』是指 2n = (−1) + (2n + 1), 2n + 1 ∈ P

最后的不成立总结『前置知识』：

*** 如果把 −1 归到质数集中, 可得命题: ***

若 −1 是质数, 则 ∀n∈ℕ₊ → 2n∈A, 且 −1 为唯一的负质数

⑴

在这里，集合 A 为所有满足两个质数之和的偶数的集合, 且此时质数包括正质数和负质数（喜感的定义出现了！）
用更偏向自然语言的方法来说，就是：

如果 -1 是质数，则对于任一正整数 n，都有：
  n 的二倍满足集合 A 的约束『元素为两个质数之和的偶数』 

⑴

  也即 n 的二倍是偶数，同时为两个质数之和

或者说（知乎用户的说法
若-1是素数，则对任意正整数n，2n属于A ⑴

*** 这个命题的逆否命题为: ***

若 ∃n₀∈ℕ₊, 2n₀∉A, 则 −1 不是质数

⑵

用更偏向自然语言的方法来说，就是：

如果 n₀ 存在于正整数集中，并且它的二倍不满足集合 A 的约束则 -1 不是质数

⑵

或者说（知乎用户的说法
若存在正整数n_0，使得2n_0∉A，则-1不是负质数 ⑵

当 n


₀

= 1 时, 若 2


∉

A, 则 −1 不是质数:

这是一个真命题, 所以该存在命题是真命题

此命题：这是一个真命题, 所以该存在命题是真命题
因为其条件（这是一个真命题）还没有得证，不能认为该存在命题是真命题
在这里，上文所指的『这』是一个命题：n₀ = 1 时 (2∉A) → (-1 不是质数)

由于原命题和其逆否命题具有等价关系, 所以原命题是真命题, 哥德巴赫猜想变式一正确


** 为什么此证明是无效的：

如果 -1 的确被定义为质数，则命题的逆反命题不为真，无法得证

如果 -1 没有被定义为质数，则命题的假设不成立，同样无法得证

Update：后来我总算看明白了，因为这一段『证明』是自相矛盾的

命题 ⑴ 假定 -1 是质数，若 -1 没有被定义为质数，则命题的假设直接不成立，无法得证
若是 -1 被定义为质数，命题 ⑴ 成立，可是，命题 ⑵ 的结论和这个假设自相矛盾，同样无法得证（命题 ⑵ 不能把一个已经成立的命题证伪，因为那是它自己证明成立的既成条件，而且这真的是相当本质的问题了，因为都不能扯到形式谬误范畴里去，否定前件（(P -> Q) -> !P -> !Q）都不是，可笑的是这种命题在数学上可以表示为复合命题 (P → ¬P)，即『由命题 P 成立可以推得命题 P 不成立』 — 这怎么可能成立呢？）

不管我们要不要把 -1 定义为质数，⑴ 和 ⑵ 都不可能同时成立，最后『由于原命题和其逆否命题具有等价关系』也就成了无稽之谈，故证明的第一部分『变式一』（式子 ⑴）在他的这个证明里就是无解的，它没有得证

所以这个证明单单从数学证明的逻辑上讲就存在谬误，这还没涉及到任何代数定理相关的问题

虽然最终的结论我懒得看是不是因为这个就不成立（因为我数学还不是很好），但我们看得出他这个证明至少有一部分已经是错的了，结合作者的表现我们可以认为此哥巴赫猜想证明无效。
信不信由你，反正我是信了。（

... 还是没有梳理明白，暂时算了

Update：从这条回答复制了一点信息过来，算是扩充

欲证：⑴。它考虑了这个命题的逆否命题：⑵。

这个逆否命题⑵是没法证出来的，因为它的结论“-1不是负质数”与之前的⑴假设“-1是负质数”矛盾。

况且，它的证明方法是：仅考虑n_0=1，此时“若”2n_0=2属于A，则-1是质数。

可以说是非常无力证明了（

作者：Monsieur TRISTE

最后这里还有一篇数学表达一点的回答，我觉得不错，可以看看

推荐这个，形式化证明从 Agda 之类的 Proof Assistant 学起，不要跟数学家们一样，自动检查多好，不需要人工（

#frontend #Unity #gamedev #Qt #desktop Qt 5 里就支持的有 Qt CSS（QSS）用来增强界面风格动态自定义的能力

CSS 注目

#Database #Data #Sysadmin #Web #Postgres #SQL #tech Transactions

呃... 其实我也不熟悉你们 DBMS 理论那一套和实践那一套，不过我作为一个普通用户来看，不是特别理解这到底坑不坑（

当然我也不知道为什么一定要 Large Object 资源必须在一个 Transaction 里被释放，他们肯定有他们的一套理由，在搞清楚他们的核心理念之前我觉得我没有资本妄加评论

Large Object 这个大家开发过 DBMS 应用的肯定都知道，就是说一个大对象

Large Objects in PostgreSQL lets you store files/objects up to 4 TiB in size.

The main benefit of using Large Objects instead of a simple column is that the data can be read and written in chunks (e.g. as a stream), instead of having to load the entire column into memory.

它有没有对应的 SQL 去查询我不知道，但就我所知可以用 oid(ObjectID) 查询，我觉得嘛，这个 API 相当有用。因为不用再把数据分为普通数据（DBMS 可存）和文件了。这样的话系统管理、备份、统计、迁移的时候肯定也方便一点，不依赖于文件系统

如果是使用 native （libpq）的程序员我觉得肯定注意得到喽，因为文档上有嘛，至于别的语言做的绑定，封装的如上面所说也都应该有提到，不过教到大家 LO 的确是个不错的实践，或许，虽然这个概念还不如一些平等数据交换、分布式、WebSocket、推送系统火



See also: [PG LO Docs, Node PGLO Binding, Source Header]

已经修改，谢谢提醒

其实 MongoDB 也有类似的东西: https://docs.mongodb.com/manual/core/gridfs/

之前用这个做爬虫的储存后端, 赛了 200 G+ 的文件（跑

感谢后端大佬的评论（

绝了

#recommended #apps #Linux #software

⌨️ 聰明的輸入法 Rime 在 2019 年迎來了大更新，重新設計了輸入法介面，並精簡了安裝包預裝的輸入方案，更方便用戶定制。
https://t.me/AppleUpgrade/28

本质上也不难理解，lo 就如同文件系统上的文件，对其操作必须「独占」该资源的控制权。在 pg 上恰好可以依赖事务机制保证操作的原子性

#learn #life #dev #pl #cs 这周的笔记 📓

有些和某些东西有关的我会转发到 Throws，至于图什么的待会发，因为照片转发到电脑上有点不方便...

+ 悲观的 2018 与形式化证明

2019 可能会是过去 10 年里最差的一年，但却是未来 10 年里最好的一年。

如何形式化地论证这个命题成立呢？

因为我现在太菜了，不是很熟练 Agda 的形式化证明，所以这可以说是 #TODO （
对不起啊，而且我也怕这花费太多时间

当然，上面我说过的那个东西后来发现其实有错误，我误会了，比如

(有火 -> 有烟) 这个复合命题是说『如果有火，那就有烟』
假设这是既成条件（它已经成立）。
但是我上面的表达是：

(有火 -> 有烟) -> 有火 -> 有虫也

其实我的目的是表示已经证明上面那个有火就有烟成立之后，由

有火 

推出

 有虫也

这是不对的，因为 (有火 -> 有烟) 是既成条件，它已经成立了，而上面那个命题实际上是说『如果』一个既成条件已经成立，这是废话。
当然这么说在上面那个文字里面没错误，但是容易引起误会

当然这些都是很 trivial 的东西，我现在正在为如何独立理解冰封博文教的归纳证明 \forall{xs}.\quad reverse \quad (reverse \quad xs) \equiv{xs} 头晕呢
其实如果不是有这篇博文，我对递归的理解不会有再次的加深，为了理解此归纳证明我以不同的可视化方式对 rev 1 :: 2 :: 3 :: [] 和它相关的东西不断弄了十几次，最后还是没能理解
当然第二天（今天）算是勉强理解了一点，但我还是无法独立证明...

+ 我妈水问题和 #PL 理论的表象类型

我妈水问题... 都知道？

女朋友对你说：我和你妈同时掉到水里，你救谁？

演讲者的意见就是这类问题不涉及实际场景是没有太大讨论意义的

我懒得把他的话再复制一遍，不过这个问题很像你们平时讨论的 C++ 和 #Java 哪个好、MySQL/Percona/MariaDB 和 PG 哪个好，GNU/Linux 和 Windows 哪个好、Vim 和 Emacs 哪个好（虽然很多人连 C-x C-b 在 Emacs 里是干啥的快捷键都不知道）

其实我的意思很明确也相当迫真，就是说，我们抽象讨论的时候就是编译器处理程序的阶段，实际处理问题的时候就是程序实际执行的时候

有些信息只有到了『运行期（runtime）』才会知道，比如一个 Java 这种经典 OOP 里参数实际的类型，而不是简单一个可以被继承，可能有 subtype （子类型）的非 final 类

所以 JIT 编译可以做一些 AOT 做不了的优化，就比如说数组访问边界检查消除，比如说分支概率预测，比如说一些运行期可以确定信息而不是常量的剪枝
（当然 AOT 也是有自己的好处的，不是 JRockit 这种面向服务器的 JVM 一般都要专门设置 server compiler JIT 编译器才敢多弄点优化措施）

相关的博文 R 大的博客上是有的，推荐阅读。不学习就会死啊！每次想着这个，learn or die 啊，说不定你就愿意学了（当然前提是你要尝试让自己相信，不学就会死，然后或许你会学（

当然，时间的朋友这演讲我觉得讲得还不错。对于一些『做实事』的人都是很有价值的。我觉得值得一看。当然是收费的（其实只是要优酷 VIP），但有价值的东西是值得你为之付费的。
如果你是 Geek 之类有些人会对这种不良心平台『恨之入骨』的，也算了，不过我觉得不是原则性问题一般都能容忍，换句话说，现在也没人能替代优酷，是不？上次知乎 #ZhiHu 的 #China #LGBT 水晶之夜（当然其实本质上是政治正确，不过它太自觉了）

就像是现在过气的新蛤社的 GoliGoli，和以前的 GeekApk，说到 #GeekApk... 绿色... 猴子... 文体两... 多多支持... 停下停下停下 🙃，当然 GeekApk 可能不会复活但我自己这个寒假（20 多天）可能独自会再起一个同样性质的项目，我不作任何担保说绝对会完成，但我相信基于我目前的表现你们会信我有完成它的技术资本。或许如果真的做出来了你们会用？（

就像曾经 @drakeet 吐槽的那样，其实 GeekApk 最大的问题在于过于功利，不像是在做事，而是很多没经验的人在瞎搅合，而真正为它写过一两行真正意义上有用代码的可能只有我和 @zhy0919(losfair) 两个人，当然我自己很冤，因为我本来不是功利的。我开始的计划虽然很幼稚，不像『做事的人』，但起码我也是细化了我的设计的，而且我从来没有计划在它完成之前就拿出去吹，或者找别人一起帮忙开发，我不指望有人能为不是自己的工程做啥贡献。自己的东西有人用都是万岁了。

虽然我那时的确是没有独立走到实现阶段的能力，但我也不只是会弱智地坐在那里想着『创建一个 Geek 社区』而无所行动，起码我是写了东西的，所以我觉得这事，谁开始『幼稚』的时候都会有的，我不后悔。

没有一个一个 '1' 积累起来也达不到 '10'，谁都不是空中楼阁。即使是天才也曾经有啥都看不懂的时候。所谓人的经历是有连续性的，不会有现在的天才是『突然开窍』而自己完全没有相关背景的说法

+ 知识的深度和广度

深度优先搜索和广度优先搜索大家都知道吧（当然我不是说这个
不过我不知道现在 #OI 生是不是所有人都会这种简单问题的，据说也有人不会？

当然现在软件工程入门门槛太低了，能模式识别，抄改代码都可以开发很优秀的 Android 应用了... 算法什么的不是必会的，你们就需要知道 Regexp.new("[\u4e00-\u9fff]*").match("字").size 可以拿来统计汉字字数，不需要知道后面 Unicode、Regex 引擎理论之类的（当然这个不是最佳实践，如果要开发实际应用的话 #Unicode 还是有些东西必须处理的，不然字数统计有问题）

所谓深度大概就是从小白（只会玩个游戏）、到用户（基本啥都不懂）、到 Geek（可能有看代码的能力）、到幼稚的开发者（抄改代码）、到普通开发者（至少会自己写复杂一点的代码了）、到企业级的开发者（有一定经验了）、到开发者依赖的开发者（知道自己真正在干什么）、到程序大师

再比如说，一个 #JavaScript 开发者可能在他自己的领域，比如 Xml/Js/AsyncIO 可能有所了解，但如果要去弄逆向工程或者 CTF 这种要求知识面和深度都有的东西，可能就啥都做不了了，他们眼里『二进制文件』和『二进制文件』... 根本没有区别嘛，而相当多一部分包括 ES6 的 JavaScript 开发者可能都没有用过 ES6 新的 ArrayBuffer

而一般来说，C/C++ 开发者的素质都比 JavaScript 开发者的素质高，我们可以认为主要写 JavaScript 的人往往比较难学会写 C/C++/C#，而写 C/C++ 之类的人全都有能力去写 JavaScript，这里我们可以看出一个深度的区别，虽然本质上还是知识面的，但从一些常见的例子看可以理解为是深度一样的东西

也就是说，深度就是从简单顺序结构到循环到递归的差别，广度大概就是同一个层次的东西了解很多，我懒得弄什么形式化定义，你们看懂就好。

最简明的代码例子（ #Kotlin ），当然因为我也很小白所以没有特别酷的例子可以弄，但我至少也不至于像王淫那样拿非常简单的 #FP 例程去骗你们说是他觉得最优雅的代码，我到觉得是他在嘲讽你们，这都看不懂 ：）
我当时就看不懂，我相信你们很多人（不是写 Scala、Clojure、Eta 的）也看不懂。

假如我们写个最简单的 FizzBuzz 程序

== 这是普通小白会写的代码，当然其实有隐含的事实，就是他们的代码是抄来的（控制结构），自己连 .. 是什么都不知道，可能

fun main(args: Array<String>) {
  for (i in 1..100) {
    if (i % 3 == 0 && i % 5 == 0)
      println(i)
  }
}

== 这是稍微有点常识的普通人（上文的『企业级开发者』）会写的代码

fun main(vararg args: String) {
  for (i in 1..100)
    if (i % 15 == 0) println(i)
}

也可能是

fun main(vararg args: String) {
  (1..100).forEach {
    x -> if (i % 15 == 0) println(i)
  }
}

之类的，看他们的觉悟了，其实这就是属于已经开始理解对算法的表述方法还有程序结构的类型了，至少他们不止了解一些『常用』的方法

== 这是又有点常识的人会写的代码

fun main(vararg args: String) = (1..100).filter { x -> x % 15 == 0 }.forEach(::println)

当然我这么说也有点迫真，其实这个例子举得不好，举例子向来都是最考验一个人技术的。

我技术不好。不过如果要举一个更好的例子，我猜是算法题。