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

*** 如果把 −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)

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

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

+ 关于 @ohcnzz 人肉李先生（李宗阳）的一些看法 #statement #China #sb （撕逼）

（当然现在某羊分享机场场主也已经承认自己是李先生了，所以这里就称他为李先生

Oh CN ZZ （就是 Telegram 版恶俗维基）这个频道的一些背后的维护者、组织者... 怎么我突然有点感觉好像里面一些人好像我还认识怎么的...

如果真的是有这样的朋友在此频道里，建议以后对像李先生

我感觉 Oh CN ZZ 现在维护起来都有点像是为了搞笑（我想，在信息安全上，随便侵犯别人隐私，随便控制别人的东西一定很兴奋，因为我也这么干过，那可真的不是一般的爽）而维护

我想它大概就是创立来泻一些人公愤的频道，但说实话，虽然李先生的确很傻逼（真的）

我觉得，就比如这次的例子，李先生是在自己的免费机场（就是科学上网的梯子）声称要打所有收费机场
想必诸如 CloudHammer 这种梯子的维护团队肯定很生气，而且远远不止这一家，所以员工们就组织起来去举着『正义』的旗帜『侵犯』李宗阳先生
但这的确是侵犯，而李先生，我觉得其实为这点事（说了句气话，但他还的确没有去打什么商业机场，只是自己独自意淫商业机场被打的情况而已）而不断挑拨他，然后维持 @OhCNZZ 更新的这种行为

最后甚至把人家身份证、百度网盘、家庭电话号码等非常隐私的东西都公开，以至于使用此机场的吃瓜群众都难以幸免被碰库（当然手段不一定是碰库，反正这里就是指尝试得到用户设置的原始明文密码这种行为）

着实不是多么令人称道（暴论）

这条消息我知道由于 Oh CN ZZ 的特殊性，内部人员肯定是不应该回复的，或许我也有误解，不过如果我的确是误会了，而李先生就是可憎的，他所受的一切就是应得的，就请大家谅解。

为小鬼说句公道话，如果以后再有类似的小鬼，我想大家都看到的时候，可以稍微忍受一下，受不了了再去弄他们也不为过（当然是要类似天安门事件的『蕞大限度的容忍』，比如迫真 DDoS 而非 DoS），但自己没有实质性的损失就去弄这种小鬼着实不好

+ 篮球很菜的

隔壁 LWL 称我『会这会那』好厉害啊（其实首先就是还没到样样通，另外的确是样样松
我真的不会打篮球... 正在学，不过我觉得学习效果还不错，别人都是打了几年的，而最近一次仅仅一两个小时我就从只能看着篮球到能够比较弱的背后传球了，并且学会了通过感知和粗略估计球体离地高度曲线和频率什么的来『救死球』，虽然那花了很久....

而之前我爸逼着我学的，是除了投篮之外啥都不会，可以说（三步上篮都没有学会

+ LWL 好大佬啊（顺路科普急救

LWL 真的好厉害啊 #life

今年做了不少社会实际活动呢，很羡慕的说

CPR （心肺复苏）的话，一些比较紧急的 case，比如身边的人心脏病突发，心脏骤停

是非常危险的，在求助、120 电话之余，若不能在 3 分钟内看到急救人员，或者无法确定时间

这时就必须实施 CPR，因为已经非常危急了，再过两分钟可能就凉了，或者就是脑死亡植物人。
这时候我觉得道德上可以说是绝对没有问题的，因为你做了别人可能就活，或者至少是最后可能醒，不做就是一个死，这种情况都是比较无奈的，那我觉得即使因为做了出现什么意外情况导致情况恶化（e.g. 实际上人家是伴随内出血，而按压加重了内出血）的，也不能说是有责任。

流程很简单

CPR involves chest compressions for adults between 5 cm (2.0 in) and 6 cm (2.4 in) deep and at a rate of at least 100 to 120 per minute

按压深度大家能自己感受到就可以了。频率是每分钟 100-120 下，就记 100 下是不会错的。
30 次按压需要辅助 2 下人工呼吸，就记大概 15 下一次也行，一个大概的频率

我相信大家虽然不是非常了解我们人类身体一些非常内部的条件机制，但至于平时容易出现的突发情况，还有一些『病症』和『解释』是做得到的（比如出车祸是什么情况，别人突然昏倒是可能什么情况），这是生物基本，小时候看过《十万个为什么》大概都知道。

+ 图解 XXX

本来 duangsuse 是想举个例子推荐大家使用图解的方式来学习，而且对我个人来说，基于这些图示分析的确是相当有效率
但 duangsuse 考虑到自己时间有限，就不教大家画了（

+ 为何我不能创作音乐？

我不是真正完全不能创作音乐，就目前而言，效率比一年前高很多很多，比较不用考虑灵感的问题（非常随性的话，不是命题作文），只不过全都是内建的... 我自己对编曲是完全没有学

其实一些简单的 Pattern，还有组合他们，我都是完全会的，不过有些东西还要经验和更好的选择能力，我以后可以考虑一下再去总结一些规律什么的...

最大的问题其实在于如何记录灵感。我对时值实在是不怎么敏感，而且我音高也达不到可以直接映射到 C4 C5 C#4 D#1 这样的水平，所以我可以说除了自己唱或者能即时能听觉反馈之外无法保持这些 pattern，没有 pattern，没有曲子...

目前还在解决这种问题，我不着急。

+ 绘画：原地打转 or 向前再出发

duangsuse 开始画一些简单的画了，主要还是铅笔的未上色 lineart 为主，水粉之类我有了数位板可以再考虑。

以前，变化是生活的一部分；现在，变化成了生活本身。——和菜头

环境在变化，时代在进步，不随着它向前，等于你落后
然而因为自己跟不上大环境而咒骂大环境为什么不止步不前的人，也太过分了吧

对于现在的软件开发者来说，要么然就像一些计算机科学爱好者一样向下钻，学会那最朴素而守恒不变的真知而后能『知其变，守其恒』，要不然就乖乖跟着时代向前走，不要老想着『学』猝死学猝死，猝死不是学习的罪，是不会安排时间的过失。

我觉得很奇怪，为什么一些工程师终日都不愿意稍微学习一下，好像一次学习就管终身了一样，产业界的一些工程师都说即便是他们一两年也会遇到一个尴尬的情况：技能纯熟了，没有挑战了

以至于自己的技术数十年如一日还是那个熊样，或者完全没有踏出自己的『领域』半步，该是前端还是前端，该是设计还是设计

自己在自满于那点『相当了解』『十分清楚』的技能树（这是 LWL 的说法，我觉得技能栈还是技能树其实都差不多，板凳条凳问题，无可厚非）时，是否有看到于自己同道的人，已经走出了『看不到自己看不到的东西有多少』的阶段，开始写各种教程甚至出书，以至于开始创建一些崭新的东西呢？而此刻，自己还在打游戏？

我觉得喜欢的东西是打游戏其实没什么，认清自己，有最起码的自知之明就是好人。虽然不是优秀的工程师，但称职的工程师也是极好的。任何看不清自己的情况，一般都会被别人引喻为无知甚至幼稚。

比如某些在 node 的 TypeScript 版继任者（可以这么说） ry/deno 那里叫板不要再更新了再学要猝死了，其实他们都知道 deno 和 node 到底是干什么的吗？还是只是把它作为一个通用的运行环境，不知道 Node 这个『Async』是什么意思，或者是只知 Async，哪怕是很简单的一些协程、并发就不会了呢？

宏观是我们必须接受的，微观才是我们可以有所作为的。——查理·芒格

遇事找客观，越找越悲观，遇事找主观，越找越乐观

客观的大环境你是没法改变的，但是你可以找你自己可以做的事情，然后去解决自己的问题，不要在无用的地方空转太多时间。

自己技术不过关以至于无法跟上时代的步伐，反而咒骂时代走得太快，我不知道这是自己的错还是时代的过失。

凡我赶不上的，我就做好准备，到未来等它。

#Telegram 这个设计比较好玩，就是如果是被别人转发的链接，即使自己被 BLOCK!!!! 了还能看？？？

#sysadmin #linux #arch #archlinux 我觉得嘛，其实 Arch Linux 还是不是特别的需要用户的系统部署管理水准的，一般人在普通 x86_64 PC 上都会比较好弄，除非是配置特殊要专门驱动的话，Gentoo 会稍微难一点，emerge 相比 pacman 概念也更复杂（当然 Gentoo 的包管理系统是叫 Portage，其实也可以说约等于 pacman + AUR，用起来稍微复杂一些），Arch 其实很友好了，建议试试。BlackArch 的话我觉得不如 Kail 好，所以还是推荐 Kali，不过 Arch 要加 BlackArch 的包们其实也可以的，但是，有时候工具的数目，开箱即用并没有那么重要

似乎 我现在格盘装 Kali 可能折腾量还少一点…或者很多
不知道是换发行版框架所带来的学习成本太高还是 Arch 本身带着一股「生人勿近」的气场

再见，我用 Kali 去了（

#dev #tech #English

boot 靴子 引导
stub 存根 占位
review 复习 评审
render 提出 渲染
map 地图 映射
console 安慰 控制台
frame 边框 帧
image 图像 镜像
bus 公交车 总线
access 入口 访问
log 伐木 日志
dump 倾倒 转储
cache 隐藏住所 缓存
port 港口 端口
performance 演出 性能— adolli🍮7️⃣🎏咕嚕靈波（●´∀｀）ノ♡ (@adolli) January 3, 2019