RecodeX 重构消息，有开发者使用Lean 4编程语言完成了RealWorld示例应用的开发。RealWorld是一个标准化的全栈应用规范，要求用不同技术栈实现同一套博客类应用功能，常被用来对比各语言与框架的工程能力。此次实现表明，以定理证明和形式化验证著称的Lean 4也能用于构建常规Web应用。