仓库 README 有一句关键原文，几乎没人引用：
"The Lean proof is a checked implication from one explicit published input: Mangerel's Theorem 1.2 in IMRN (2024)... this does not remove the explicit Mangerel hypothesis."
翻译：Lean 验证的是"若 Mangerel 定理成立，则 4 的倍数版本成立"这个蕴含关系——Mangerel 定理是作为显式输入/假设引入的，并没有被重新证明。审计确认无 sorry 、无新增公理，这是真的；但它验证的是条件性蕴含，不是从零开始的完整证明。
整体之所以仍算"无条件"，是因为 Mangerel 那条定理本身是无条件的 。
Comments
这个主要贡献还是那个24年的文章吧（但主要是他24年那个文章的证明感觉也是假设＝N-1得到各种各样的等式然后一通分析，力大砖飞的那种），我觉得单纯是那个作者没有看出来这个推论（虽然我去年看了这个文章啥也没看出来）
♥ 48 ↩ 2
最接近哥德巴赫猜想结果的，依然是筛法得到的1+2，最多三个质数最少两个质数就可以表示出一个偶数，这也是筛法的极限
♥ 42 ↩ 12
这个结果比哥德巴赫猜想弱多了，但是这个证明挺美妙的。。
♥ 28
对哥猜本体影响不大
♥ 12
OpenAI 的模型已经斩杀了真仙的一具分身[doge]
♥ 11 ↩ 8
这文章都达不到Acta Arithmetica…..
♥ 10 ↩ 8
文章是人用OpenAI 的模型写的，又不是OpenAI 公司写的，妥妥标题党
♥ 5
ai至今写不好论文。。。[藏狐]
♥ 5 ↩ 8
up 是你吗[doge]
♥ 2 ↩ 1
只有奇偶性障碍被完全绕过或者突破才能证明这玩意儿
♥ 2
这是 openai 公司发的？
♥ 2
可以先解释一下Liouville型哥德巴赫猜想和原本哥德巴赫猜想的联系。
♥ 2 ↩ 4
他不一定不是open ai的内部人员吧。
♥ 2
。[吃瓜]
♥ 2
首评[doge]
♥ 2
5度LAB也是打卡上了[doge]
♥ 2 ↩ 1
之前的成果，比如1+3不能直接推出这个结论吗？
♥ 2 ↩ 4
仓库 README 有一句关键原文，几乎没人引用： "The Lean proof is a checked implication from one explicit published input: Mangerel's Theorem 1.2 in IMRN (2024)... this does not remove the explicit Mangerel hypothesis." 翻译：Lean 验证的是"若 Mangerel 定理成立，则 4 的倍数版本成立"这个蕴含关系——Mangerel 定理是作为显式输入/假设引入的，并没有被重新证明。审计确认无 sorry 、无新增公理，这是真的；但它验证的是条件性蕴含，不是从零开始的完整证明。 整体之所以仍算"无条件"，是因为 Mangerel 那条定理本身是无条件的 。
♥ 1 ↩ 2
现在都说拿ai写论文，结果数学上已经做通了，把关键步骤都码进去了，希望ai补全，结果写的一坨，全删也不至于，多少有点可取之处。于是变成了我们给ai改论文，最后费的时间太多，根据经验，比我们从零开始手工写，费的时间都多。
♥ 1 ↩ 1
该成果的价值不如解决困难的竞赛题
♥ 1