GoKawiilDeveloper builds full RealWorld reference app entirely in Lean 4
A developer created a complete implementation of RealWorld, the Medium-clone reference application used to benchmark full-stack frameworks, using only Lean 4, a functional language best known as a proof assistant. The project includes a server, database integration, and frontend rendering, and passes RealWorld's official API and website test suites. The frontend uses a library called datastar-lean for interactivity, and the full source code is published on GitHub.