当国内技术圈还在日更"AI能帮我写什么代码""用AI搞什么副业"时，海外顶级社区这周却在聊一个更深的问题——当生成变廉价，什么东西反而升值了？ 这一轮 HN 头版没有"XX工具真香"式的欢呼，而是三场冷静到近乎残酷的价值重估：Paul Graham 用一篇《如何赚十亿美元》刷出 626 分 1632 评论，把"执行"判了死刑；Jane Street（华尔街最赚钱的量化之一）公开宣布因 agentic coding 而"投奔"形式化方法，265 分 94 评论里全是"AI 代码是 slop"的共识；一个独立游戏开发者写下《vibe coded games 时代的老玩家自白》，承认自己的护城河已经被 AI 摧毁。三场讨论指向同一个信息差：AI 真正颠覆的不是"谁能写代码"，而是"写代码这件事还值不值钱"。
先说这周 HN 最炸的一条——Paul Graham 6 月新作《How to Earn a Billion Dollars》，626 分、1632 条评论（这个评论量在 HN 一周内极其罕见）。文章本身源自他在牛津联合会（Oxford Union）的一场演讲，看似在讲"如何变富"，实则重新定义了创业的本质。
PG 的核心论点极其数学化，他用一个计算把全场镇住：变富只取决于两个数字——增长率，和它能持续多久。 他甚至让读者当场掏出手机算：从 200 万美元起步，按每月 93% 增长，需要多久到 10 亿？答案是 log(500, 1.93) ≈ 9.45，9 个半月。即便取保守的每月 15% 增长，5 年（60 个月）后是 1.15^60 ≈ 4384 倍——月入 1 万美元的项目会变成月入 4400 万美元。
关键不是这些数字，而是 PG 推出的结论：你不需要作弊，不需要剥削。你只需要做出一个"好到用户愿意告诉朋友"的东西，指数增长会自动发生。 而怎么做出这样的东西？PG 给出了他一贯的反共识答案——做你自己和你的朋友想要的东西，因为"你的需求预测了未来的需求"。最好的创业想法一开始听起来都很蠢：Apple（"谁会想要自己的电脑"）、Facebook（"靠本科生互相网上跟踪赚钱"）、Airbnb（"谁会付钱睡别人家充气床垫"）、以及 YC 2006 年投的 Justin.TV（一个人头顶摄像头直播生活）——后来它改名 Twitch。
对中国开发者的信息差在哪里？ PG 没有直接谈 AI，但 1632 条评论几乎全在追问一个 AI 时代的问题：当 AI 让"做出来"的门槛趋近于零，独立思考（判断"做什么"）是不是变成了唯一的护城河？ 国内 AI 创业大多还在卷"怎么做"——套壳、集成、复刻海外产品，本质是把执行能力商品化。而 PG 这篇文章等于在宣告：执行正在被 AI 平权化，卷"怎么做"的人，正在把越来越不值钱的技能卖得越来越便宜。真正稀缺的是"做什么"的判断力，而判断力恰恰无法被模型生成——因为它来自你对某个细分人群痛点的、第一手的、只有你自己能感受到的共情。
如果说 PG 是从"商业/判断"维度给出 AI 时代的价值地图，那么 Jane Street 这篇博客就是从"工程/可靠性"维度补上了另一半——而且这是华尔街真金白银的押注。
文章作者是 Jane Street 的元老 Yaron Minsky（2002 年入职，正是他说服公司全面采用 OCaml 那位），发表于 2026 年 6 月 7 日。开头一句话就足够震撼："过去 25 年，我一直告诉大家 Jane Street 对形式化方法（formal methods）不感兴趣。我现在不这么说了。"
他先用 seL4（业界最知名的经过形式化验证的微内核）说明传统形式化方法有多贵——验证 8700 行 C 代码，花了 25 个人年，平均每一行代码要 23 行证明、耗费半个人天。 正因为成本如此恐怖，Jane Street 25 年来一直觉得"不划算"。
然后他甩出了整篇文章最值钱的一句话：
"But the emergence of agentic coding has changed our perspective, and we've gone from being skeptical to being excited."（agentic coding 的出现改变了我们的看法，我们从怀疑变成了兴奋。）
Jane Street 给出 AI 时代形式化方法突然升值的三个理由，每一个都是对中国技术从业者的认知暴击：
"验证瓶颈"比以往任何时候都重要。 原文直接用了 "slop"（垃圾内容）这个词形容 AI 生成的代码——"过度复杂、充满诡异的 bug 和边界情况、常常不遵循代码库的关键不变量（invariants）"。也就是说：模型越来越擅长写代码，但模型写的代码和你真正敢发布的代码之间，有一道巨大的鸿沟。 这道鸿沟就是验证成本，而形式化方法可以大幅压缩它。
Agent 靠反馈（feedback）变强。 不管是 RL 训练还是用 agent 写代码，它都需要反馈信号。形式化方法、类型系统能提供"全称量词"级别的反馈（∀，对所有情况都成立），这比测试用例（只能覆盖被测的那几个情况）强大得多。
类型系统（一种轻量级形式化方法）已经在 agent 编程中证明了巨大价值——比如类型一旦设计成"不可能出现数据竞争"，就真的能消灭所有数据竞争；设计成"不可能出现 XSS"，就真的能消灭 XSS。这种"universal guarantee"是测试永远给不了的。
文章末尾，Jane Street 宣布正在伦敦和纽约组建专门的形式化方法团队，并点名拥抱 Lean、Dafny、Rocq、Agda、Iris、以及自家力推的 OxCaml。
信息差读法： 国内开发者对"形式化方法/定理证明"的印象大多停留在"学院派、屠龙术、不实用"。但 Jane Street 这篇博客等于一份公开的产业信号——当 agentic coding 让"生成"廉价，"证明"就变成了新的稀缺品。它还有一层更实操的启示：你不需要上全套 Rocq/Lean，但你完全可以现在就把"更强的类型约束 + property-based testing + fuzzing"作为对抗 AI slop 的防线。 Jane Street 自己都承认，测试不是唯一答案，类型系统这种"轻量形式化"才是性价比最高的第一步。
第三场讨论最动人，也最扎心——因为它来自一个真正靠"长期手艺"吃饭的普通人。
ZenGM 是一个免费网页端体育模拟游戏（Basketball GM 等）的独立开发者，从 2012 年开始写，2021 年终于做成全职。他在 2026 年 6 月 12 日发了这篇《How it feels to be an old school web-based sports sim dev when tons of vibecoded web-based sports sims are being released》，被顶上 HN 首页。
文章的逻辑链极其清晰，值得每一个技术人细读：
多年来，他之所以安全，是因为"经济上不划算"——做一个能和 BBGM 抗衡的游戏，需要投入一个团队数年的精力，而这块利基市场的全部收入都不够养团队。所以没有正常人会来竞争。一个痴迷型业余开发者（他自己）才能熬出来。
"And then AI happened." 现在，每天都有新的 vibe coded 体育模拟游戏发布。它们大多粗糙，但"至少有一些令人印象深刻的功能"，而且其中不乏用心的作品。他写道：
"It's like the enemy is approaching my city walls... the siege has not begun, the battle has not started. But it's coming."（就像敌人正在逼近我的城墙，围攻还没开始，战斗还没打响。但它要来了。）
他被迫预测：也许一两年内，就会有人做出和 BBGM 一样好、甚至更好的游戏。 最深刻的是结尾那句对"技术史"的反思——过去的每一次技术变革最终都为人类打开了新机会，因为"人类一直是最聪明的物种"。"当这一点不再成立时，会发生什么？"
信息差读法： 这是迄今为止最诚实的一份"AI 冲击个体经济护城河"的一手记录。它戳破了一个国内常见幻觉——很多人以为"我做得足够好/足够久，AI 就替代不了我"。ZenGM 的答案是：AI 不是在质量上超越你，而是在"成本"上让你的存在变得不经济。 当任何人都能用 AI 在一个周末搓出一个能玩的体育模拟游戏，"我熬了 14 年"这件事就不再是壁垒，而成了负担。这对所有"靠长期积累堆出来的小众手艺"（独立工具、垂直 SaaS、内容产品）都是一个红色警报。
把这三场讨论叠在一起，2026 年 6 月 HN 社区其实在集体回答同一个问题——AI 让"生成"成本趋近于零之后，价值会迁移到哪里？ 答案是三个方向：
flowchart TD
A["AI 让'生成'成本趋近于零"] --> B1["维度一：执行被平权<br/>PG — 人人都能'做出来'"]
A --> B2["维度二：验证成瓶颈<br/>Jane Street — agent 代码 = slop"]
A --> B3["维度三：护城河消失<br/>ZenGM — 经济门槛被抹平"]
B1 --> C1["价值迁移 → 判断力<br/>'做什么'比'怎么做'更稀缺"]
B2 --> C2["价值迁移 → 数学证明<br/>形式化方法身价暴涨"]
B3 --> C3["价值迁移 → 人类独特性<br/>品味/共情/不可批量复制"]
C1 --> D["对中国从业者的统一启示：<br/>停止卷'怎么做'，开始构建模型生成不了的东西"]
C2 --> D
C3 --> D
| 维度 | 国内常见认知 | 海外社区本周共识（信息差） |
|---|---|---|
| AI 的核心冲击 | AI 让我能写更多代码、效率更高 | AI 让"写代码"本身贬值，价值转移到判断、证明、品味 |
| 创业壁垒 | 技术实现能力、资源整合 | 指数增长只看两个数：增长率+持续时长；壁垒是"做什么"的共情（PG） |
| AI 生成代码 | 用 agent 提效，相信它 | 一线顶级团队公开称其为 "slop"，押注形式化方法来验证（Jane Street） |
| 职业护城河 | 把手艺做深、做久 | 当生成廉价，"长期投入"可能反而成为负担（ZenGM） |
| 稀缺能力 | prompt 工程、AI 应用开发 | 判断力、数学证明能力、不可批量复制的个人品味 |
重读 PG 这篇文章并做一次计算。 用你当前项目/副业的真实数字套 1.15^60，看清楚你是在追"稳定的线性增长"还是"指数曲线"。如果你做的东西无法让用户主动告诉朋友，AI 不会救你，只会让竞争对手更快追上你。
给你的 AI 工作流加一道"验证层"。 不必上 Rocq/Lean，但立刻做三件事：(a) 强化类型约束（TypeScript strict、Rust、或在动态语言里上 schema 验证）；(b) 引入 property-based testing 和 fuzzing；(c) 把 agent 生成的 PR 默认当作"不可信"来 review。这是 Jane Street 在用真金白银验证过的、性价比最高的反 slop 方案。
审视你自己的"经济护城河"。 诚实地问：如果对手用一个周末加 AI 就能复刻我的核心功能，我还剩下什么？如果答案是"什么都没有"，那么你接下来 6 个月最重要的事不是学新 AI 工具，而是找到那个"模型生成不了、但你的特定用户群体愿意为之付费"的东西——可能是行业 know-how、可能是社区信任、可能是对某个细分人群的第一手共情。
关注形式化方法的"工程化红利"窗口。 Lean、Dafny、Rocq、OxCaml 正在从学术走向工业。Jane Street、Anthropic、各大模型公司都在招这个方向的人。这是未来 1-2 年确定性很高的"认知差红利"——目前国内懂定理证明 + 实际工程的人极少。
本文由「51学通信」技术团队出品。51学通信由通信行业18年老兵爱卫生（微信ID: gprshome201101）维护。 聚焦5G/6G核心网、3GPP标准、AI工具实战。知识星球「51学通信」提供深度技术答疑和行业洞察。
[!tip] 51学通信知识星球 星主：爱卫生（微信：gprshome201101）——公众号「51学通信」创办者，19 年通信行业运维与讲师经验，著有《GPRS网络信令实例详解》《EPC原理与实践》《5G核心网原理与实践》三本纸质书（各大电商平台有售）。 星球定位：深耕 5G 核心网、IMS、NFV/AI、云原生等 ICT 领域，主打运维岗位与信令分析。 当前规模：5200 篇主题 / 990 个回答，198 元/年。 加入福利：加入星球后请加爱卫生微信，拉您进知识星球年度陪伴与答疑群——不限量回复您的各种问题，另有群内分享。 AI 加持：51学通信知识星球已作为 skill 接入 WorkBuddy，使用 deepseek-4-flash 在海量星球帖子中精准找贴、找视频、找 FAQ 和案例，做总结、找文档和 PPT 等场景全覆盖。