统计信息
- 无权查看
- 浪浪山的宣发出人意料地不做人，可惜了这部好片子
回复 - 浪浪山小妖怪出人意料地好看，推荐一下
回复 - 说一个小米产的好东西吧。米家驱蚊器，前后一共买了五个，价格分别为60，69，69，118和122元。现在已停产，京东上能买到的最低价是542元
回复 - 纯血鸿蒙已经可用。新的更新里有卓易通，基本上所有的安卓APP都能自行安装了。 回复
- 握手，我们楼也封了，5天后解封 回复
回复- 回复
- 恭喜恭喜 回复
- 爱坛里问一下，有人用过Intel的NUC吗？噪音到底大不大？一直长草这个NUC，就是这个噪音问题让我犹豫。 回复
- 折腾了两天，AdoptOpenJDK不支持Isabelle 2020，只好换回Oracle的Java SE JDK 11.0.8。 回复
唐家山 发表了新日志 点评一下最近用到的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的建模和构造能力，但是不要指望它们的自我纠错能 ...
- 三“英”战吕布 2026-02-14
- 最近用AI做定理证明太投入，一不小心把Gemini的额度用完了。趁着等待Gemini重置额度的时间，我把正在证的一个证明分别在多个AI上面试了一下。办法很简单，初始是 ...
- 点评一下最近用到的AI工具 2026-02-12
- Gemini 3.0 Pro：是最为全面和稳健的，是我在定理证明时用到的主要工具。但是这个工具太有自己的主见了，经常把问题复杂化，而且会陷在某个特定细节中出不来。当 ...
- 关于AI辅助交互定理证明 2026-02-01
- 最近在做AI辅助的交互式定理证明，又有了一些新的发现： 1. AI带来的效率提升是有上限的。 2. 你做不到的，AI也做不到。 3. 多AI交互可能是处理复杂问题的最 ...
- 无语了 2026-01-20
- 这段时期在做一个大的证明。已经把框架和几个主要目标证完了，让AI帮忙把最后一个目标的对应引理写出来。 AI很快给出了引理的内容和证明梗概，我想着最后一个目 ...
- 看了知乎的两个帖子 2026-01-12
- 感觉真是长见识了。 一个帖子是duolou的： 为什么唯物主义在全世界竞争不过宗教? - duolou的回答 - 知乎 中国人恰恰不是纯的 唯物主义 ，很多人也提到了，纯 ...
- 看了mingxiaot兄的史海钩沉 2025-12-17
- 突然有点感慨。大浪淘沙这个词非常残酷。 按照历史唯物主义的说法，人类自身的行为是不能大幅超出人类社会当时的生产力水平和认知水平的。如果有，也是非常态。 ...
应用
现在还没有应用
最近访客
