即刻App年轻人的同好社区
下载
置顶大家好，我是 Liz，新人报道！🥳
我是应用数学出身，这些年在大型国企、互联网大厂、顶级咨询公司都打过卡，算是把国内大厂生态体验了一轮。早年沉迷算法，从传统机器学习一路卷到 NLP 和图算法，最近几年又扎进了生成式 AI。虽然是 90 后，但从本科起就开始研究数据和算法，也算是完整见证了大数据和 AI 十多年的风云变幻（叉腰.jpg）。
一路走来，我做过算法工程师、全栈工程师、架构师，再到 AI 产品负责人。现在在一家外企担任 Data Science Manager，带团队从业务需求出发，用一年时间把 GenAI 数据产品从 0 到 1 落地上线。我关注模型性能，更关注产品价值和用户体验，需求定义、用户访谈、交互设计，这些我工作中的常态，致力于打造真正“好用”的 AI 产品🥰。
工作之外，我也热衷于探索更多可能性：参与开源项目、构建内部工具、写脚本提升效率。我喜欢健身与户外运动，十多年跑步爱好者，跑过几场马拉松😄，正在学咏春，运动带来的专注与节奏感也深刻影响了我的工作方式。
目前我和 @Xinran.Z 共同发起了非营利社区Research AI+ ，聚集了一群来自全球的 AI 4 Science / Engineering 青年研究者。我们专注于 AI for Research 的实践与讨论，也在推动产业与学术的深度交流。近期我们正在长三角组织线下沙龙与论文共读等活动，欢迎感兴趣的朋友一起参与交流！
我是应用数学出身，这些年在大型国企、互联网大厂、顶级咨询公司都打过卡，算是把国内大厂生态体验了一轮。早年沉迷算法，从传统机器学习一路卷到 NLP 和图算法，最近几年又扎进了生成式 AI。虽然是 90 后，但从本科起就开始研究数据和算法，也算是完整见证了大数据和 AI 十多年的风云变幻（叉腰.jpg）。
一路走来，我做过算法工程师、全栈工程师、架构师，再到 AI 产品负责人。现在在一家外企担任 Data Science Manager，带团队从业务需求出发，用一年时间把 GenAI 数据产品从 0 到 1 落地上线。我关注模型性能，更关注产品价值和用户体验，需求定义、用户访谈、交互设计，这些我工作中的常态，致力于打造真正“好用”的 AI 产品🥰。
工作之外，我也热衷于探索更多可能性：参与开源项目、构建内部工具、写脚本提升效率。我喜欢健身与户外运动，十多年跑步爱好者，跑过几场马拉松😄，正在学咏春，运动带来的专注与节奏感也深刻影响了我的工作方式。
目前我和 @Xinran.Z 共同发起了非营利社区Research AI+ ，聚集了一群来自全球的 AI 4 Science / Engineering 青年研究者。我们专注于 AI for Research 的实践与讨论，也在推动产业与学术的深度交流。近期我们正在长三角组织线下沙龙与论文共读等活动，欢迎感兴趣的朋友一起参与交流！
26 70
昨天参加了一个 Product Mindset 的 workshop，我们一起做了一轮 User Interview 的 retrospective，回顾整个访谈流程，这时发生了一件很有意思的事情。
我突然想起 @玉伯 老师前几天在demo day 分享里提到的一句话——“人是环境的反应器。”意思是说，做产品的本质，是为用户构造一个环境。
当时我觉得这句话适用于产品设计，没想到在用户访谈时突然 pop up。我们不是在“提问”，而是在营造一个真实的、让用户放松且进入状态的场域。比如展示一个具体的例子或小 demo，用户往往会从“回忆”状态切换到“再体验”，我们也就更容易听到背后的真实动机——这其实就是在构造物理环境。
而心理环境的构建同样重要。用户访谈并不是“被测试”，也不是“闲聊”，而是一种让对方产生“我可以讲真话”的信任感。作为访谈者，我们需要拿捏好理性与感性的平衡：理性让问题更聚焦、更有洞察力；感性则能让用户放松、卸下防备。但太理性可能让访谈显得冷硬，太感性又容易跑偏，因此这种“度”的把握，其实非常关键。
我把这个想法分享给 workshop 的 mentor，他觉得很有道理。他还补充说，有一个很实用的提问技巧就是——无论你想问什么，可以多用“我很好奇你是怎么……”作为开头。这样既能保持对话的理性结构，又带着好奇与尊重的语气，更容易让用户进入状态。
访谈本身，也是一种“产品设计”。构建的不是功能，而是一个让用户讲真话的空间。
我突然想起 @玉伯 老师前几天在demo day 分享里提到的一句话——“人是环境的反应器。”意思是说，做产品的本质，是为用户构造一个环境。
当时我觉得这句话适用于产品设计，没想到在用户访谈时突然 pop up。我们不是在“提问”，而是在营造一个真实的、让用户放松且进入状态的场域。比如展示一个具体的例子或小 demo，用户往往会从“回忆”状态切换到“再体验”，我们也就更容易听到背后的真实动机——这其实就是在构造物理环境。
而心理环境的构建同样重要。用户访谈并不是“被测试”，也不是“闲聊”，而是一种让对方产生“我可以讲真话”的信任感。作为访谈者，我们需要拿捏好理性与感性的平衡：理性让问题更聚焦、更有洞察力；感性则能让用户放松、卸下防备。但太理性可能让访谈显得冷硬，太感性又容易跑偏，因此这种“度”的把握，其实非常关键。
我把这个想法分享给 workshop 的 mentor，他觉得很有道理。他还补充说，有一个很实用的提问技巧就是——无论你想问什么，可以多用“我很好奇你是怎么……”作为开头。这样既能保持对话的理性结构，又带着好奇与尊重的语气，更容易让用户进入状态。
访谈本身，也是一种“产品设计”。构建的不是功能，而是一个让用户讲真话的空间。
17 24
最近看了《黑镜》第七季的第一集《Common People》，虽然早有听说这集情绪压抑，但还是决定一看究竟。看完后，确实心情很复杂。
这集延续了《黑镜》一贯对技术与社会关系的敏锐洞察，但与以往不同的是，它对现实的贴近感更强。AI、脑机接口、云意识订阅等设定虽然看似未来，但实际已经和我们当下正在发生的趋势有很多相似点。
看完之后，我去看了很多讨论，担心错过什么细节。发现最多人争议的是：一个月 300 美元的意识“订阅费”到底算不算贵？有人觉得对于现在的美国大部分民众来说不算什么。但我觉得，这个设定其实是对未来贫富差距极度不平衡的一种影射，是普通人在技术与资本交织下被吞噬的预演。
你看男主拼命地加班，在 “Dum Dummies” 上进行近乎羞辱式的直播，拼尽全力只能换来几十刀、几百刀，这不是努力不够，而是身处财富极度不均时代下的无力挣扎。普通人的生存变得艰难，努力变得廉价，甚至连“活着”这件事本身，都成了需要被“订阅”的特权。
而且这集让我联想到一个正在发生的现实趋势：当AI快速发展、自动化重塑劳动结构时，我们也看到全球范围内人文学科的边缘化愈加明显。文科招生人数下降、社会对其价值认同减弱，背后其实反映出我们对“如何更好的使用和平衡技术与人文”这件事的关注正在削弱。
但事实上，人文学科——尤其是伦理、社会学、哲学——本质上是在提供一套“提问能力”和“规范框架”。它们提醒我们技术不只是效率和产出，也关乎选择、边界与责任。如果技术的扩张缺少这些视角的参与，我们可能会加速走向一个只有工具理性、缺乏公共价值的系统。
AI 本身是中性的加速器，它可以增强创造力、提升效率，也可能放大结构性不平等或短期利益导向。关键在于，我们是否在技术发展的同时，也保留了对“人”的关注与思辨。
我并非人文学科出身，也不自认为能深入探讨伦理问题。但作为一名科技从业者，我想这种跨学科的反思还是是非常必要的——哪怕只是提出一个问题，或者keep an eye on this.
这集延续了《黑镜》一贯对技术与社会关系的敏锐洞察，但与以往不同的是，它对现实的贴近感更强。AI、脑机接口、云意识订阅等设定虽然看似未来，但实际已经和我们当下正在发生的趋势有很多相似点。
看完之后，我去看了很多讨论，担心错过什么细节。发现最多人争议的是：一个月 300 美元的意识“订阅费”到底算不算贵？有人觉得对于现在的美国大部分民众来说不算什么。但我觉得，这个设定其实是对未来贫富差距极度不平衡的一种影射，是普通人在技术与资本交织下被吞噬的预演。
你看男主拼命地加班，在 “Dum Dummies” 上进行近乎羞辱式的直播，拼尽全力只能换来几十刀、几百刀，这不是努力不够，而是身处财富极度不均时代下的无力挣扎。普通人的生存变得艰难，努力变得廉价，甚至连“活着”这件事本身，都成了需要被“订阅”的特权。
而且这集让我联想到一个正在发生的现实趋势：当AI快速发展、自动化重塑劳动结构时，我们也看到全球范围内人文学科的边缘化愈加明显。文科招生人数下降、社会对其价值认同减弱，背后其实反映出我们对“如何更好的使用和平衡技术与人文”这件事的关注正在削弱。
但事实上，人文学科——尤其是伦理、社会学、哲学——本质上是在提供一套“提问能力”和“规范框架”。它们提醒我们技术不只是效率和产出，也关乎选择、边界与责任。如果技术的扩张缺少这些视角的参与，我们可能会加速走向一个只有工具理性、缺乏公共价值的系统。
AI 本身是中性的加速器，它可以增强创造力、提升效率，也可能放大结构性不平等或短期利益导向。关键在于，我们是否在技术发展的同时，也保留了对“人”的关注与思辨。
我并非人文学科出身，也不自认为能深入探讨伦理问题。但作为一名科技从业者，我想这种跨学科的反思还是是非常必要的——哪怕只是提出一个问题，或者keep an eye on this.
14 34
DeepSeek 果然在五一假期的最后一刻放了一个大招，发布了最新的模型：DeepSeek-Prover-V2（模型链接）。或许是因为假期原因，又或许这次不像上次那样伴随“破纪录”级的 result-driven 效果，感觉媒体上讨论的不多？不过我之前读过他们的第一篇论文，对他们的论证思路印象很深刻。这次趁着假期休息，我认真读完了这篇新论文，越读越觉得有趣，于是写下这篇读书笔记，和大家一起分享一下：
我会从两个角度来讲这篇论文：
1. 简单介绍论文的主要思路和技术路线；
2. 分享我觉得特别有意思的几个点，尤其是它如何连接“人类的思考方式”和“机器的逻辑严谨”。
一、研究背景：为什么“形式化证明”是 LLM 的下一块硬骨头？
大语言模型（LLM）在解数学题时已有不俗表现，尤其是在使用 Chain-of-Thought（逐步推理）策略下。但这些自然语言推理路径，本质上仍属于非形式、依赖直觉和启发式的思维。相比之下，形式化证明系统如 Lean、Coq 要求每一步推导都必须严谨、显式、可验证。这就引发一个核心挑战：LLM 擅长“人类语言的模糊表达”，但计算机需要“机器语言的绝对严谨”——怎么在中间搭桥？
二、论文方法概览：从自然语言到 Lean 代码的递归构造
1. 冷启动数据构造：CoT + Lean 子目标（Subgoals）
使用通用模型 DeepSeek-V3 对定理进行理解与子目标分解，输出 Chain-of-Thought + 多个 have := sorry 结构；然后使用一个精简版的 7B 模型递归补全每个子目标，拼接后构成完整的 Lean 证明；最终生成成百上千条包含推理链与可验证证明的冷启动样本。
2. 课程学习 + 强化学习（GRPO）
通过 curriculum learning 逐步喂给模型越来越难的问题；使用 Group Relative Policy Optimization（GRPO）训练模型，在保证验证正确的同时，还奖励与原始推理路径结构对齐的解法；
两种模式并行训练：
· CoT 模式：强调推理路径与解释性；
· non-CoT 模式：高效 Lean 代码生成。
三、我觉得特别有意思的地方
1. 模型不再“瞎猜”，而是真的在做逻辑闭环
大模型以前在解数学题时，总给人一种“答对了但说不出为什么”的感觉。这篇论文让模型写的 Lean 代码真的能过验证，每一步都是严格推理的结果。这从“语言生成”迈向了“推断生成”。
2. 子目标分解就像一个 AI 数学博士的写作习惯
人类做数学证明常常先写一个“proof sketch”，也就是先列一个解题提纲和大致步骤，再逐步展开证明每个步骤。这个系统也是模拟这个思路设计的，先使用DeepSeek-V3 对定理进行理解与子目标分解， 然后使用小模型证明每个子目标：先写出 lemma1 := sorry，然后再一条条补全。这种结构化的方式极大减少了搜索空间。
3. 7B 小模型竟然在一些题目上赢了 671B 大模型
在 Putnam 竞赛题中，7B 模型成功解出 13 个大模型解不出的题。原因是它用了大模型没有掌握的一些“冷门技巧”（如 Cardinal.toNat 处理集合大小），这说明小模型可能更容易产生“非主流但有效”的推理路径。
4. 非形式与形式化推理的差距在缩小
DeepSeek-V3 解了 8 道 AIME（自然语言形式），而 DeepSeek-Prover-V2 解了其中 6 道的 Lean 形式化版本。这是目前为止最接近“自然语言理解”与“严谨证明构造”的对比，显示了语言模型推理能力的进一步融合。
四、实验成绩非常亮眼
DeepSeek-Prover-V2 成绩 ：miniF2F-test Pass@8192 88.9% ，ProofNet-test Pass@1024 37.1%， PutnamBench Pass@512 49 / 658 ，AIME 24&25 的15 题中解出 6题。此外，作者还构建了新的 ProverBench 数据集，包括 325 道来自教材和竞赛的 Lean 形式题，是非常有价值的研究资源。
五、从“会说话”到“会证明”，LLM 又进了一大步
这篇论文系统性地构建出了一条从自然语言思考到形式化逻辑表达的路径。我们知道，语言模型本质上是在做“下一个 token 的概率预测”，而这其实与数学家的思维方式并不矛盾。作为一个数学背景出身的人，我非常能共鸣这种过程：它就像是人们对一个定理最初产生的“数感”——一种模糊但有方向的直觉。而真正的数学能力，不止于此。在大量训练数据的滋养下，这种“感知”会逐渐沉淀为一个严谨的证明框架，这个框架既能帮助我们在逻辑上走得更稳健，也能将我们的思维成果与他人共享和验证。而 DeepSeek-Prover-V2 做的，就是将这种“模糊感知到清晰框架”的路径，变成了机器也能走通的通路。它不只是让模型“看起来像在推理”，而是让它真的像数学家一样地证明。
未来，也许我们真的能见到一个 AlphaZero 式的自动数学系统：它不是靠背过题库、套模板，而是靠真正的逻辑推理能力，去实现推导，探索，发现。
我会从两个角度来讲这篇论文：
1. 简单介绍论文的主要思路和技术路线；
2. 分享我觉得特别有意思的几个点，尤其是它如何连接“人类的思考方式”和“机器的逻辑严谨”。
一、研究背景：为什么“形式化证明”是 LLM 的下一块硬骨头？
大语言模型（LLM）在解数学题时已有不俗表现，尤其是在使用 Chain-of-Thought（逐步推理）策略下。但这些自然语言推理路径，本质上仍属于非形式、依赖直觉和启发式的思维。相比之下，形式化证明系统如 Lean、Coq 要求每一步推导都必须严谨、显式、可验证。这就引发一个核心挑战：LLM 擅长“人类语言的模糊表达”，但计算机需要“机器语言的绝对严谨”——怎么在中间搭桥？
二、论文方法概览：从自然语言到 Lean 代码的递归构造
1. 冷启动数据构造：CoT + Lean 子目标（Subgoals）
使用通用模型 DeepSeek-V3 对定理进行理解与子目标分解，输出 Chain-of-Thought + 多个 have := sorry 结构；然后使用一个精简版的 7B 模型递归补全每个子目标，拼接后构成完整的 Lean 证明；最终生成成百上千条包含推理链与可验证证明的冷启动样本。
2. 课程学习 + 强化学习（GRPO）
通过 curriculum learning 逐步喂给模型越来越难的问题；使用 Group Relative Policy Optimization（GRPO）训练模型，在保证验证正确的同时，还奖励与原始推理路径结构对齐的解法；
两种模式并行训练：
· CoT 模式：强调推理路径与解释性；
· non-CoT 模式：高效 Lean 代码生成。
三、我觉得特别有意思的地方
1. 模型不再“瞎猜”，而是真的在做逻辑闭环
大模型以前在解数学题时，总给人一种“答对了但说不出为什么”的感觉。这篇论文让模型写的 Lean 代码真的能过验证，每一步都是严格推理的结果。这从“语言生成”迈向了“推断生成”。
2. 子目标分解就像一个 AI 数学博士的写作习惯
人类做数学证明常常先写一个“proof sketch”，也就是先列一个解题提纲和大致步骤，再逐步展开证明每个步骤。这个系统也是模拟这个思路设计的，先使用DeepSeek-V3 对定理进行理解与子目标分解， 然后使用小模型证明每个子目标：先写出 lemma1 := sorry，然后再一条条补全。这种结构化的方式极大减少了搜索空间。
3. 7B 小模型竟然在一些题目上赢了 671B 大模型
在 Putnam 竞赛题中，7B 模型成功解出 13 个大模型解不出的题。原因是它用了大模型没有掌握的一些“冷门技巧”（如 Cardinal.toNat 处理集合大小），这说明小模型可能更容易产生“非主流但有效”的推理路径。
4. 非形式与形式化推理的差距在缩小
DeepSeek-V3 解了 8 道 AIME（自然语言形式），而 DeepSeek-Prover-V2 解了其中 6 道的 Lean 形式化版本。这是目前为止最接近“自然语言理解”与“严谨证明构造”的对比，显示了语言模型推理能力的进一步融合。
四、实验成绩非常亮眼
DeepSeek-Prover-V2 成绩 ：miniF2F-test Pass@8192 88.9% ，ProofNet-test Pass@1024 37.1%， PutnamBench Pass@512 49 / 658 ，AIME 24&25 的15 题中解出 6题。此外，作者还构建了新的 ProverBench 数据集，包括 325 道来自教材和竞赛的 Lean 形式题，是非常有价值的研究资源。
五、从“会说话”到“会证明”，LLM 又进了一大步
这篇论文系统性地构建出了一条从自然语言思考到形式化逻辑表达的路径。我们知道，语言模型本质上是在做“下一个 token 的概率预测”，而这其实与数学家的思维方式并不矛盾。作为一个数学背景出身的人，我非常能共鸣这种过程：它就像是人们对一个定理最初产生的“数感”——一种模糊但有方向的直觉。而真正的数学能力，不止于此。在大量训练数据的滋养下，这种“感知”会逐渐沉淀为一个严谨的证明框架，这个框架既能帮助我们在逻辑上走得更稳健，也能将我们的思维成果与他人共享和验证。而 DeepSeek-Prover-V2 做的，就是将这种“模糊感知到清晰框架”的路径，变成了机器也能走通的通路。它不只是让模型“看起来像在推理”，而是让它真的像数学家一样地证明。
未来，也许我们真的能见到一个 AlphaZero 式的自动数学系统：它不是靠背过题库、套模板，而是靠真正的逻辑推理能力，去实现推导，探索，发现。
https://aicraftlab.substack.com/p/from-language-models-to-theorem-proving?utm_source=activity_item
5 10
刚刚快速试了一下哪个产品用来识别流程图的精度更高，快速地对比了Gemini 和MinerU，Gemini
真的是能够理解流程图的含义，MinerU直接放弃了（是我打开方式不对么？🤣）
真的是能够理解流程图的含义，MinerU直接放弃了（是我打开方式不对么？🤣）
1 10
最近 openai 推出了 codex cli，默认需要 openai api key，但是因为众所周知的原因，这对于国内的同学不太友好，下面的教程是能够使用openrouter的 api key，这样国内的同学也能自由是尝试啦（下面是Macbook指令）～～
1. "npm i -g open-codex" ## 使用 npm 将名为 open-codex 的包 全局安装 到你的电脑上
2. nano ~/.codex/config.json ## 打开 config 文件进行编辑
3. 将下面内容填入上面这个文件
```
{
"provider": "openrouter",
"model": "openai/gpt-4o"
}
```
4. echo 'export OPENROUTER_API_KEY="你的openrouter api key"' >> ~/.zshrc ## 将OPENROUTER_API_KEY放入你的配置文件
5. source ~/.zshrc ## 让配置文件生效
6. 在 terminal 输入：open-codex ## 你可以自由的玩耍啦
1. "npm i -g open-codex" ## 使用 npm 将名为 open-codex 的包 全局安装 到你的电脑上
2. nano ~/.codex/config.json ## 打开 config 文件进行编辑
3. 将下面内容填入上面这个文件
```
{
"provider": "openrouter",
"model": "openai/gpt-4o"
}
```
4. echo 'export OPENROUTER_API_KEY="你的openrouter api key"' >> ~/.zshrc ## 将OPENROUTER_API_KEY放入你的配置文件
5. source ~/.zshrc ## 让配置文件生效
6. 在 terminal 输入：open-codex ## 你可以自由的玩耍啦
15 82
早上地铁上读到 Andrew Ng 关于评估（evals）的一篇文章，让我重新思考了很多。
他说很多团队会因为觉得前期评估工作量太大，而迟迟不开始。但评估不一定要等到系统稳定后再做，也不需要一次性铺得很完备。哪怕只是从 5 个样本、一个粗糙的指标开始，都可以逐步积累、持续改进。
我深有同感。在我们当前的开发节奏下，项目推进非常快，需求层出不穷，很多时候都是“先上线、再修补”。作为项目负责人，我需要权衡技术和产品需求，我也确实很清楚评估机制的重要性。但现实是：每一轮迭代周期都很短，大家优先关注的是功能是否可交付、流程能否跑通，评估这一块就很容易被搁置，成为“之后有空再做”的任务。
但这种“之后再做”的方式，其实是把这头“评估的大象”越养越大。比如一开始如果我们能在每一轮加入几个样本评估、设计一个简单的成功判别逻辑，其实可以很快形成最初的反馈闭环；但如果一直等着“评估体系完整再做”，最后就会变成一次性需要投入大量精力去还“技术债”的局面。
而且我们也越来越发现，光靠人判断模型效果是撑不住的。模型行为越来越复杂，输出越来越长，团队成员对“什么是好”的标准也会逐渐分歧，没有一套基本的自动评估体系，后期维护和优化的效率会明显下降。
评估这件事，其实不是额外的负担，而是基础建设的一部分。与其把它看成一个庞大的、压在头顶的大项目，不如将它“拆象为块”，在每一轮迭代中做一点点。每多加 5 个样本，每补一个自动 check，就能逐渐缩小模型和人之间的评判差距，也能让系统在长期中更稳、更准。
写下来，一方面提醒自己：不要被“完美主义”或“时间压力”劝退评估的必要性；另一方面也希望未来的每一个项目中，都能更早地为评估预留出空间。
Andrew 原文链接见下图（发现有链接发不出来🤣）
他说很多团队会因为觉得前期评估工作量太大，而迟迟不开始。但评估不一定要等到系统稳定后再做，也不需要一次性铺得很完备。哪怕只是从 5 个样本、一个粗糙的指标开始，都可以逐步积累、持续改进。
我深有同感。在我们当前的开发节奏下，项目推进非常快，需求层出不穷，很多时候都是“先上线、再修补”。作为项目负责人，我需要权衡技术和产品需求，我也确实很清楚评估机制的重要性。但现实是：每一轮迭代周期都很短，大家优先关注的是功能是否可交付、流程能否跑通，评估这一块就很容易被搁置，成为“之后有空再做”的任务。
但这种“之后再做”的方式，其实是把这头“评估的大象”越养越大。比如一开始如果我们能在每一轮加入几个样本评估、设计一个简单的成功判别逻辑，其实可以很快形成最初的反馈闭环；但如果一直等着“评估体系完整再做”，最后就会变成一次性需要投入大量精力去还“技术债”的局面。
而且我们也越来越发现，光靠人判断模型效果是撑不住的。模型行为越来越复杂，输出越来越长，团队成员对“什么是好”的标准也会逐渐分歧，没有一套基本的自动评估体系，后期维护和优化的效率会明显下降。
评估这件事，其实不是额外的负担，而是基础建设的一部分。与其把它看成一个庞大的、压在头顶的大项目，不如将它“拆象为块”，在每一轮迭代中做一点点。每多加 5 个样本，每补一个自动 check，就能逐渐缩小模型和人之间的评判差距，也能让系统在长期中更稳、更准。
写下来，一方面提醒自己：不要被“完美主义”或“时间压力”劝退评估的必要性；另一方面也希望未来的每一个项目中，都能更早地为评估预留出空间。
Andrew 原文链接见下图（发现有链接发不出来🤣）
9 38
狂风暴雨天，适合一起当流水线女工debug🤣 ，一不留神就到了这个点，还没结束@Xinran.Z
4 00