用 Lean4 在线游戏玩转逻辑学与类型论
V2EX 社区有开发者推荐通过 Lean4 在线游戏中的“A Lean Intro to Logic”和“Reintroduction to Proofs”模块来上手逻辑学与类型论。对熟悉 TypeScript 或 C++ 类型推导的开发者来说，这种互动形式既有挑战性也很有趣。Lean4 虽然主打数学形式化证明，但基于“柯里-霍华德同构”原理，程序代码与数学证明在本质上相通。每天花时间过一关，通常一两周就能通关，能直观体验严谨的类型推导与逻辑证明，适合对编程语言底层理论感兴趣的开发者。