统计信息
- 无权查看
- 浪浪山的宣发出人意料地不做人，可惜了这部好片子
回复 - 浪浪山小妖怪出人意料地好看，推荐一下
回复 - 说一个小米产的好东西吧。米家驱蚊器，前后一共买了五个，价格分别为60，69，69，118和122元。现在已停产，京东上能买到的最低价是542元
回复 - 纯血鸿蒙已经可用。新的更新里有卓易通，基本上所有的安卓APP都能自行安装了。 回复
- 握手，我们楼也封了，5天后解封 回复
回复- 回复
- 恭喜恭喜 回复
- 爱坛里问一下，有人用过Intel的NUC吗？噪音到底大不大？一直长草这个NUC，就是这个噪音问题让我犹豫。 回复
- 折腾了两天，AdoptOpenJDK不支持Isabelle 2020，只好换回Oracle的Java SE JDK 11.0.8。 回复
唐家山 发表了新日志 VcXsrv 远程界面模糊的解决方案
遇到几次这个问题了，在日志里记录一下。 找到 VcXsrv 的安装目录或启动快捷方式（通常为 vcxsrv.exe，默认在 C:\Program Files\VcXsrv）。 右键点击文件， ...- 唐家山 发表了新日志 从V2Ray到Xray
又需要全局翻墙了。我熟门熟路地安装了V2RayA客户端，然后翻墙失败了。 这次有大模型帮忙，问了一下大模型，才知道现在v2ray已经过气了，现在是Xray的时代。 赶 ... - 唐家山 发表了新日志 点评一下最近用到的AI工具
Gemini 3.0 Pro：是最为全面和稳健的，是我在定理证明时用到的主要工具。但是这个工具太有自己的主见了，经常把问题复杂化，而且会陷在某个特定细节中出不来。当 ... - 唐家山 发表了新日志 关于AI辅助交互定理证明
最近在做AI辅助的交互式定理证明，又有了一些新的发现： 1. AI带来的效率提升是有上限的。 2. 你做不到的，AI也做不到。 3. 多AI交互可能是处理复杂问题的最 ... - 唐家山 发表了新日志 看了mingxiaot兄的史海钩沉
突然有点感慨。大浪淘沙这个词非常残酷。 按照历史唯物主义的说法，人类自身的行为是不能大幅超出人类社会当时的生产力水平和认知水平的。如果有，也是非常态。 ... - 唐家山 发表了新日志 AI辅助做定理证明的几点心得（续）
受蚊行启发，我也开始同时用DeepSeek和Gemini辅助进行定理证明。有时候让它们进行交叉验证。 Gemini给出的证明框架更简洁，DeepSeek对证明细节的把控更好。 如 ... - 唐家山 发表了新日志 DeepSeek的元验证感觉是通向AGI的关键一步
这是知乎AI对元验证（Meta-Verification）的评述： Meta-Verification是指在验证AI生成的证明或解题步骤时，引入更高一层的验证机制，即给原本的验证者（AI老 ... - 唐家山 发表了新日志 AI辅助做定理证明的几点心得
1. 提前写出非形式的证明。这一点最关键。后面需要反复用这些非形式证明与AI进行交互，给出提示。 2. 相信AI的建模和构造能力，但是不要指望它们的自我纠错能 ...
- VcXsrv 远程界面模糊的解决方案 2026-06-23
- 遇到几次这个问题了，在日志里记录一下。 找到 VcXsrv 的安装目录或启动快捷方式（通常为 vcxsrv.exe，默认在 C:\Program Files\VcXsrv）。 右键点击文件， ...
- 从V2Ray到Xray 2026-04-10
- 又需要全局翻墙了。我熟门熟路地安装了V2RayA客户端，然后翻墙失败了。 这次有大模型帮忙，问了一下大模型，才知道现在v2ray已经过气了，现在是Xray的时代。 赶 ...
- 现场播报 2026-03-10
- 两个AI自己吵起来了，一个说对方欺骗了自己，一个说对方是胡说八道。 而我，差点又被带进了一个大坑。还好我还保持着朴素的物理直觉，否决了某个AI的建议。 言 ...
- 硅基生物的“人性” 2026-03-06
- 这个题目怎么这么别扭呢？我是想说AI跟人一样，也有偷懒的天性。 如果遇到自己能搞定的证明，那证明代码写的是洋洋洒洒，连标点符号都能给你排版好。 但是如果 ...
- 别把豆包不当干粮 2026-03-05
- 之前我评估AI的推理能力时，说豆包不具备基本的文本解析能力。后来发现是我自己没找对地方 ，豆包是能够进行多文本文件解析的。 昨天Gemini突然暂停了服务，我差 ...
- 双雄记 2026-03-04
- 我最早是用DeepSeek开始做vibe proving的，后来项目做大了，DeepSeek的上下文窗口不够，用的主力工具转向了Gemini。 现在DeepSeek更新了百万上下文的版本后，我 ...
