科技爱好者周刊（第 412 期）：禁止 issue，只用 PR
内容提要
本期周刊聚焦 Laravel 禁止提交 issue、只收 PR，认为可减少垃圾反馈、方便维护者，AI 时代提交 PR 已不困难。Anthropic 用 Claude 历时11天将怀尔斯费马大定理证明译为 Lean 语言，生成1300万行代码，为史上最长数学程序。此外还介绍特斯拉 Cybercab、戴森电动牙刷、AI 手杖等科技动态，以及多篇文章、工具、资源和言论。
延伸解读
禁止 issue 的深层逻辑
Laravel 禁止 issue 只收 PR，表面看是提高门槛，实则针对开源项目资源不足的痛点。垃圾 issue 和机器人骚扰消耗维护者精力，而 PR 至少经过一定思考。AI 时代，用户可借助 AI 生成 PR，提交难度并未增加。这一变化鼓励用户从“抛问题”转向“做贡献”，可能成为资源紧张项目的可行策略。
AI 证明费马大定理的意义
Claude 用 11 天将怀尔斯的 129 页证明翻译成 Lean 语言，生成 1300 万行代码，证明超过 3 万个辅助定理。这不仅是史上最长数学程序，更表明 AI 能验证复杂数学证明，解决人工验证耗时费力的问题。数学界可借此自动化检查证明，但陶哲轩也提醒，AI 大量解题可能消耗不可再生的数学问题，影响数学思维发展。
特斯拉 Cybercab 的商业模式风险
特斯拉出售 Cybercab，买家需额外购买 15000 美元的自动驾驶功能包，并承担车辆折旧。特斯拉则从重资产转向轻资产，与车主对半分载客收入。这种模式让车主投资，但全天运营的车辆寿命有限，能否盈利存疑。它反映了特斯拉主营转向无人驾驶出租车的战略，但实际回报需市场检验。
产品开发的三问原则
文摘提出开发前需问三个问题：能否一页纸写清介绍、核心技术能否与产品分离、产品有无核心特色。这能避免产品过于复杂或缺乏个性。例如手机的核心技术是移动通信，产品可迭代但技术持续。核心特色如 Minecraft 的方块，能缩小决策空间。若无法肯定回答，则不应开发，以防臃肿。
Q&A
Laravel 为什么禁止提交 issue，只允许提交 PR？
Laravel 认为禁止 issue 只收 PR 可以减少垃圾反馈，方便维护者从 PR 中获取更多信息，且 AI 时代提交 PR 几乎和提交 issue 一样简单。根本原因是开源项目资源不足，应付不了激增的 issue，应鼓励用户一起贡献而非抛问题。
Anthropic 用 Claude 完成了什么数学程序？耗时和代码量如何？
Anthropic 用 Claude AI 历时 11 天，将安德鲁·怀尔斯对费马大定理的证明翻译成 Lean 语言程序，生成了 1300 万行代码，先证明了超过 3 万个辅助定理，消耗数十亿 Token，成为史上最长的数学程序。
特斯拉 Cybercab 的出售模式是怎样的？购买后如何盈利？
特斯拉在美国推出 Cybercab 出租车并对外出售。购买者不是为了自己乘坐，而是作为投资，每次载客收入与特斯拉对半分。车辆 24 小时运营，但购买者需承担折旧贬值，还需另购 15000 美元的自动驾驶功能包。
哈佛大学发明的 AI 手杖如何帮助视障人士？
AI 手杖需配合手机使用，手机利用摄像头、GPS、运动和方向传感器捕捉实时数据，结合导航软件确定方向并传给手杖。手杖发出哔哔声提示前进、左转或右转，走错方向时发出警报声。
在开始构建产品前应该问自己哪三个问题？
（1）能不能把产品介绍写成一页纸的概要？超过一页说明太复杂。（2）核心技术能不能与产品分离？核心技术应始终如一并持续发展。（3）产品有没有一个核心特色？特色赋予产品独特个性，缩小决策空间。三个问题都肯定才开发。
陶哲轩对 AI 解决数学难题有什么担忧？
陶哲轩认为，人们让 AI 大量解决数学难题，但数学难题不可再生，如今好的问题已变得稀缺。自动化工具解题并没有增加人类的数学思维，反而损害了未来的数学发展。
