用Lean 4构建RealWorld：数学证明写Web
I built the RealWorld app in Lean 4
我尝试用Lean 4构建了一个完整的RealWorld应用，包括前端和后端。Lean 4通常被视为证明助手，但如今其标准库已支持HTTP服务器，社区也在开发Postgres驱动、加密和HTML渲染等库。我通过实现RealWorld验证了这一点：整个应用约1600行代码，比TypeScript、Go和C#版本更短。文章以数学论文风格呈现，强调类型安全与形式化验证。虽然大部分代码由Claude Code生成，但核心逻辑和关键属性都经过Lean的严格证明。尽管当前生态尚年轻，存在稳定性和性能限制，但只要控制流量、锁定工具链并人工审查代码，它已具备服务真实用户的能力。
正确性源于构造，而非测试——尤其是当AI编写了大部分代码时。
- saviorand
我一直想知道 Lean 4 是否已经能用于日常 Web 应用开发，而不仅仅是写证明。所以我用 Lean 4 构建了一个 RealWorld（Medium 克隆版），包含前端，使用了 Datastar。看起来借助新的库，现在这已经可行。这篇帖子描述了整个体验过程。
- hiAndrewQuinn
这是个极好的消息。去年我研究过将 Lean 用于通用软件开发，发现它在库方面还欠缺不少，所以像 leanpostgres 已经可用这样的消息是一个巨大的进步。
- solomonb
Lean 4 的秘密在于它其实是一门很棒的编程语言，有点像超级版的 Haskell。事实上，作为编程语言，我比作为证明检查器更喜欢它！
依赖类型不仅对形式验证很有用，对常规编程来说也棒极了。至于证明检查，我其实更偏爱 Agda。