我用 Lean 4 写了一个 RealWorld 应用

一位开发者用 Lean 4 完整实现了 RealWorld 参考应用（Medium 克隆），前端也用 Lean 编写，交互依赖 datastar-lean，代码已开源在 GitHub。