推荐试试 lean4 在线游戏 的 A Lean Intro to Logic 和 Reintroduction to Proofs 两个章节。
尤其是后者“依值类型论”，非常适合喜欢 TypeScript 或 C++ 类型推导的强迫症患者。有些关卡很烧脑，但尽量不要搜答案或问 AI ，自己想出来会非常有成就感~
虽然 lean4 原用于数学证明，但根据“柯里-霍华德同构”（ Curry-Howard Isomorphism ），计算机程序与数学证明本质上是同一件事。有兴趣的可以试试。
⚠️内容来自互联网，如有侵权请点击反馈！侵权投诉
2#SYS宇晖
之前只听说 lean 是做数学证明的，没想到跟 TS 类型推导能扯上关系。
[这只是一个小尾巴]
3#卷王
我觉得，计算机程序是数字电子，数学证明，是模拟电子。CPU 是数字型，但给 CPU 供电的主板，vrm 模块，确实模拟电子。CPU 预测接下来有大动作，要求大功率，VRM 给了大功率，大电压，结果 CPU 因为缓存 miss ，导致计算任务其实很小，那电已经来了，怎么办，只能靠 vrm 来泄压。而且，电压变动，会导致波动，出现 undershoot 和 overshoot ，所以有了 CPU 缩肛。还没看 op 的网站。