统计信息
- 无权查看
- 浪浪山的宣发出人意料地不做人，可惜了这部好片子
回复 - 浪浪山小妖怪出人意料地好看，推荐一下
回复 - 说一个小米产的好东西吧。米家驱蚊器，前后一共买了五个，价格分别为60，69，69，118和122元。现在已停产，京东上能买到的最低价是542元
回复 - 纯血鸿蒙已经可用。新的更新里有卓易通，基本上所有的安卓APP都能自行安装了。 回复
- 握手，我们楼也封了，5天后解封 回复
回复- 回复
- 恭喜恭喜 回复
- 爱坛里问一下，有人用过Intel的NUC吗？噪音到底大不大？一直长草这个NUC，就是这个噪音问题让我犹豫。 回复
- 折腾了两天，AdoptOpenJDK不支持Isabelle 2020，只好换回Oracle的Java SE JDK 11.0.8。 回复
唐家山 发表了新日志 看了mingxiaot兄的史海钩沉
突然有点感慨。大浪淘沙这个词非常残酷。 按照历史唯物主义的说法，人类自身的行为是不能大幅超出人类社会当时的生产力水平和认知水平的。如果有，也是非常态。 ...- 唐家山 发表了新日志 AI辅助做定理证明的几点心得（续）
受蚊行启发，我也开始同时用DeepSeek和Gemini辅助进行定理证明。有时候让它们进行交叉验证。 Gemini给出的证明框架更简洁，DeepSeek对证明细节的把控更好。 如 ... - 唐家山 发表了新日志 DeepSeek的元验证感觉是通向AGI的关键一步
这是知乎AI对元验证（Meta-Verification）的评述： Meta-Verification是指在验证AI生成的证明或解题步骤时，引入更高一层的验证机制，即给原本的验证者（AI老 ... - 唐家山 发表了新日志 AI辅助做定理证明的几点心得
1. 提前写出非形式的证明。这一点最关键。后面需要反复用这些非形式证明与AI进行交互，给出提示。 2. 相信AI的建模和构造能力，但是不要指望它们的自我纠错能 ... - 唐家山 发表了新日志 微信公众号转存pdf时图片缺失的问题
看到一篇微信公众号的文章写的不错，想转成pdf文件收藏。 结果发现另存为pdf时图片都不见了。问了DeepSeek，写了一个python程序，确实可以从网页转成pdf，但是由 ... - 唐家山 发表了新日志 说一个小米产的好东西吧，米家智能驱蚊器
前后一共买了五个，价格分别为60，69，69，118和122元。现在已停产，京东上能买到的最低价是281元。 米家智能驱蚊器用的驱蚊片是oem安速的。但是安速驱蚊器没 ...
- 看了mingxiaot兄的史海钩沉 2025-12-17
- 突然有点感慨。大浪淘沙这个词非常残酷。 按照历史唯物主义的说法，人类自身的行为是不能大幅超出人类社会当时的生产力水平和认知水平的。如果有，也是非常态。 ...
- AI辅助做定理证明的几点心得（续） 2025-12-02
- 受蚊行启发，我也开始同时用DeepSeek和Gemini辅助进行定理证明。有时候让它们进行交叉验证。 Gemini给出的证明框架更简洁，DeepSeek对证明细节的把控更好。 如 ...
- DeepSeek的元验证感觉是通向AGI的关键一步 2025-11-28
- 这是知乎AI对元验证（Meta-Verification）的评述： Meta-Verification是指在验证AI生成的证明或解题步骤时，引入更高一层的验证机制，即给原本的验证者（AI老 ...
- AI辅助做定理证明的几点心得 2025-11-20
- 1. 提前写出非形式的证明。这一点最关键。后面需要反复用这些非形式证明与AI进行交互，给出提示。 2. 相信AI的建模和构造能力，但是不要指望它们的自我纠错能 ...
- 继续折腾验证工具 2025-10-01
- 书接上回。我不是把验证工具安装好了吗，但是使用的时候有一处麻烦。就是在证明时需要用一些工具内置的功能。这些功能如果用鼠标来操作，一点问题都没有。比方说 ...
- 有感两则 2025-10-01
- 1. 有一句话是：某人（组织）成功地解决了只有他（们）才会发生的问题。当时是当笑话听的。现在看来这句话不一定是贬义。能解决问题就很厉害了，历史又成功向前 ...
