26-10-18周记：用 Deeptotur 搭配 DeepSeek 学高中竞赛，并启动 SF-lean4 项目

前言

这是本人最近一个星期思考与规划的合集，包含了在学校多天的内容。
本文也可以理解为一篇周记。
聆听《勾指起誓》的同时阅读此文体验更佳～

whk 部分

背景

十月一外培回来后这是我第一次高中的月考，本次月考我考的也是很差好吧。
年级排名 rk 270，班级排名 rk 37.
综合来看，原因是我开学后一直在训练 OI，没咋学 whk。
不过鄙人确实找到一个学习 whk 的好方法，那就是学习对应科目的竞赛教材。
（这里引用一句我们化学老师说的话：“大学的公式不是让你大学学的，而是不学就上不了大学”）
既然，OIer 在做 leetcode 时如鱼得水，那么 MOer 做数学、PhOer 做物理肯定也是这样的感觉。
理论成立，开始实践。

方法

那这个时候就要请出大名鼎鼎的 Deeptotur 了，这是一个 AI 学习框架，具体而言它可以为你制定相当详细的学习计划，并且通过对话来教你，中途也会出题。
使用它的前提是你有一个模型的 API，在 deeptotur 配置好就可以使用了，这里推荐 deepseek 的模型，便宜好用。
随后呢，就是展现我们 prompt 技术的时候了，打开精通之旅，新建一个目标，随后写一个描述，在对话中输入：
“请你根据高中 xx 科目课本及竞赛教材，制定一个知识点数量在 200 以上，难度逼近 IMO/IPhO/IBO/IChO，总学习时长约 6-12 个月”
随后你就可以开始学了，中途可以调整难度。
但请注意，此方法对于学习者的数学基础要求很高，为此，在数理化生四科里，数学是最重要的，优先推进数学的学习。
在需要配合图片理解时，可以直接让他画图；另外如果进行了考试，可以把考试卷子导入让其分析。
OK 那么这是我目前在使用的工具，我会测试一学期来看成果。

思考部分

关于 AI 的局限性

就我目前想到的缺点包括：
1.无法识别反话
2.不能记住用户特殊要求的同时不一直重复该要求（比如你提了一个不是很常见的要求它就会在之后的回答中一直往上面靠）
3.无法做到平实表述而不是堆砌词汇
4.在 OI 或者数学中无法出那种具有精妙构造和包装的题目，大部分都是短平快的。

关于左手练字

那么熟悉我的人都知道我的字还算可以，右手练了瘦金体和行楷。
那么有没有可能也练一下左手呢？当然可以啦，这个可以在抖音搜索 Cccccccc 来证明。
于是乎从初四开始我断断续续的练了半个月的左手行楷，最近又开始持续的练习，终于有了些起色。
从此次练习不难看出，练字最重要的其实是控笔，字形是其次的，排版是再次的。
而且右手学会的字形可以无缝迁移到左手来使用。

何为好题

设有一些常见技巧、操作、变形为 \(f(x),g(x),h(x)\) 。
普通题：\(f(x)\) 或 \(g(x)\) 或 \(h(x)\)
普通的难题：\(f(x)+g(x)+h(x)\)
好题：\(f(g(h(x))),f(g(x),h(x)),(f(x)g(x))'\)
换言之，好题需要出题人发现几个技巧中的共有结构，并以此使几个技巧依托这些结构无缝融合，而不是复合。

关于一些文摘

“因为人区别于猪的地方在于，总会不地抬起头来仰望天空。” ————《飞向太空港》

杂项

关于博客

好久不写了呢，之前每次写都是发生了大事才写，从今天开始打算每周都写了。

关于逆袭导论

这是我去年这个时候就开始写的一本书。
去年它还是一篇短文章，今年 8 月份我进行了重构，使用 latex 进行了重写，增加了很多内容，达到了 3w 字左右。
那么这第二版仍然不完美，于是我准备从现在开始就攥写第三版。
具体而言有如下的要求：
1.去除 AI 味，将 AI 写的内容全部手动重写；
2.增加更多关于我个人经验的部分，尤其是练字和中长跑；
3.增加选学章节，如 LLM 原理简介、计算机原理简介、逻辑学入门；
4.加入上文提到的以竞赛应对 whk 的方法；
5.加入关于处理压力、恋爱相关的部分；
6.增加更多的图片；
7.增加关于黑色生命力、精力管理的章节；
8.增加更多图片，推荐更多资料、音乐、博主；
9.重写道德修养章节，新增更多的方法论；
10.进行整体重排，优化表达。

关于已有的素材

“熟识我的人和第一次见我的人都认为我不太爱笑，确实是这样的，一般而言，他们见到的我都是十分高冷的样子。
这是因为，能让我发自内心高兴的只有三种事，和喜欢的人有关的、和自己或团队或国家或人类的成就有关的、和为人民服务有关的。
也有人看到我难得满面春风，一边笑一边走路，这大概是我刚刚遇到了上述三件事的后两个之一，譬如我刚刚帮助了一个陌生人，又或者是 CTorch 有了新的进展，这时的我，毫无疑问是这个世界上最开心的人之一。
那为什么没有第一个呢，这是因为第一类事情我大概会躲起来自己偷偷的笑，有可能会笑一整天（逃）。
……
如果你心情不好，那么试着去帮助一个陌生人，相信我，你会笑的比任何人都要灿烂。”
————《逆袭导论》v3 草稿

关于形式化证明

众所周知，lean 4 与 Coq 一直是形式化证明的两个主流语言。
而 lean 4 最近使用更加频繁，更加激进而现代，coq 则历史悠久，资料齐全。
其中最重要的问题在于《软件基础》这本书是没有 lean 4 版本的。
那么对于我这样的拥有大量用不完的 token 的人来说，发起一个把 SF 转为 lean 4 版本的项目是很有必要的，于是乎，SF-lean4 这个项目就诞生了。
这也和本文结语追求的内涵是一致的。

结语

“追求难以想象的成就，而不是难以达成的成就”