有没有对“逻辑学”和“类型论”感兴趣的？

• 请不要在回答技术问题时复制粘贴 AI 生成的内容

推荐试试 lean4 在线游戏的 A Lean Intro to Logic 和 Reintroduction to Proofs 两个章节。

尤其是类型论，非常适合喜欢 TypeScript 或 C++ 类型推导的强迫症患者。有些关卡很烧脑，但尽量不要搜答案或问 AI ，自己想出来会非常有成就感~

虽然 lean4 原用于数学证明，但根据“柯里-霍华德同构”（ Curry-Howard Isomorphism ），计算机程序与数学证明本质上是同一件事。有兴趣的可以试试~ 前面的入门题目很容易，后面关卡会难一点，每天挑战一题，大约一两周就可以通关。

逻辑学

类型论

证明

4 replies • 2026-11-05 20:23:20 +08:00

archxm

10h 31m ago

我觉得，计算机程序是数字电子，数学证明，是模拟电子。

CPU 是数字型，但给 CPU 供电的主板，vrm 模块，确实模拟电子。
CPU 预测接下来有大动作，要求大功率，VRM 给了大功率，大电压，结果 CPU 因为缓存 miss ，导致计算任务其实很小，
那电已经来了，怎么办，只能靠 vrm 来泄压。而且，电压变动，会导致波动，出现 undershoot 和 overshoot ，所以有了 CPU 缩肛。

还没看 op 的网站。

tool3d

9h 57m ago

@archxm 德文的网站,应该不是楼主大神的.
我玩了一下,以前就有人说类似楼主这种大神,天天写大家看不懂的代码,玩看不懂的游戏,现在总算是切身感受到了.

MindMindMax

7h 21m ago

看标题点进来，原以为你要讨论的是哲学。。。

iqoo

6h 0m ago

@MindMindMax 也算是哲学吧，用代码写哲学。口头讨论没法严谨判定，lean 可以直接判定结果对不对。