I built the RealWorld app in Lean 4

Lately its standard library has also gained an HTTP server. The community is writing the other libraries that ordinary apps need too, like Postgres drivers, cryptography and HTML rendering.So can you build a real web app in Lean yet? I built RealWorld in it to find out. RealWorld is a well-known reference app, a Medium clone that comes with official test suites for its API and its website. My version is written entirely in Lean including the frontend, which uses datastar-lean for interactivity. The code is on GitHub.I’ve written this post like a math paper, mostly because it’s fun and partly because it keeps the structure clear. Most of what follows is still plain engineering of the kind you would do in any language. The few things that are actually proved are marked as propositions. Lean checks those proofs every time the code builds.2ExistenceThe first question is whether a RealWorld app can be built in Lean at all. The test suites turn that into something we can check.Definition 1. A RealWorld implementation is a program that passes RealWorld’s API suite and its website suite1.Theorem 1. There is a RealWorld implementation in Lean.The proof is to build one. The test suites define what it has to do. The API tests send HTTP requests and check the JSON that comes back, so we need a server. The data in those answers has to be kept between requests, which means a database. The website tests click through the site in a real browser, so the server has to render pages as well.Construction 1 (The server). Lean’s standard library has had an HTTP server, Std.Http, since April. It takes care of all the low-level connection handling for you. On top of that server I use lean-routing to declare the API’s routes in a table. Each route has a path with typed parameters and gets its own handler.

.delete patterns.comment (deleteComment env), ... ]This handler deletes a comment. It checks the user’s login token with requireUser, calls the service layer to delete the comment and replies with 204 No Content. The website calls the same service layer and therefore follows exactly the same rules. Everything else comes from libraries, as it would in any language: lean-json for JSON lean-libcrypto for hashing passwords with OpenSSL's scrypt lean-jose for the login tokens (JSON Web Tokens) lean-middleware for CORS, cookies and static files Construction 2 (The database). The data lives in Postgres. I talk to it through leanpostgres, which wraps Postgres’s C client and keeps a pool of connections. You write the SQL right in the code. Each row that comes back is turned into a Lean structure:def userByEmail (db : Conn) (email : String) : IO (Option UserRow) := do first (← db sql!"SELECT id, username, email, password_hash, bio, image FROM users WHERE email = {email}")The {email} inside sql! becomes a query parameter, which Postgres receives separately from the SQL text. So user input can never run as SQL. The database schema is plain SQL that leanmigrate applies when the server starts.Construction 3 (The website). The pages are rendered on the server with lean-html. There are no templates because the HTML is written as ordinary Lean functions. This one shows a comment, plus a trash icon if you wrote it:def commentCard (viewer : Option Db.UserRow) (slug : String) (c : Db.CommentRow) : Node .flow := let delete : List (Node .phrasing) := if viewer.any (·.id == c.authorId) then [ span [ i [] { class_ := "ion-trash-a" } ] { class_ := "mod-options" } [onClick (action "delete" (Site.links.comment slug c.id.toInt.toNat))] ] else [] div [ div [ p [ c.body ] { class_ := "card-text" } ] { class_ := "card-block" }, ... ] { class_ := "card", id := s!"comment-{c.id}" }That onClick is all the frontend code needed to delete a comment. Datastar, a small script on the page, sends the DELETE request when you click the icon. It then updates the page with the server’s reply. The server builds that reply with the same function the JSON API uses. There’s no frontend build step because the pages are just HTML plus one script.

Code written this fast hasn’t had many readers or users yet. So the kind of bugs you only find in real use are probably still in there.The easiest parts to trust are the types and the theorems, because Lean checks them. Those hold no matter who or what wrote the code. The instructions the libraries give their AI agent push in this direction.

Code that no theorem covers is only as reliable as its tests. That goes double for the bindings to C libraries, where Lean can’t check the C code at all.You still need to read the proved parts, though. Lean checks that each proof is correct, but it can’t check whether the theorem states what you actually need. Agents asked for proofs often prove things that don’t matter. When Dan Luu had coding agents implement Zstd compression and told them to use Lean 4, they mostly proved arithmetic facts that missed the bug-prone code. Those proofs didn’t make the code any more correct8. So you still have to read all of it, theorems and proofs included. Check that it does what you need and fix it where it doesn’t. Don’t trust any part you haven’t checked yourself.Tools like claimcheck can help with that reading. It has an AI model restate each theorem in plain English without knowing what the theorem was meant to say. A second step compares that restatement with the original intent9. It’s a useful check, but it doesn’t replace reading.Partial answer to Question 2. So can the app serve real users? Yes, as long as three things hold: (H1) traffic stays modest, (H2) you pin the toolchain, and (H3) someone actually reads the code. The server’s limits don’t matter while traffic stays modest. You can also run several copies of the app for more load because it keeps no state between requests. A pinned toolchain means a new Lean release can’t break anything until you choose to upgrade. Reading the code is doable where it matters most because the app is only about 1,600 lines. Someone should read its handlers, its SQL and its C bindings carefully before real users see them.4CorrectnessI think correctness by construction is what you should aim for, especially when an AI writes most of your code. It means first writing down exactly what the program should do in a formal language. The code is then derived from that description in steps that are each proved correct.Today most people rely on tests instead, or hand the agent a spec and hope it follows it. Tests only check the cases someone thought to write. Dan Luu’s experiments also show that agents write poor tests, even when told which technique to use. A spec on its own can’t show that the code actually follows it. Correctness by construction closes that gap, because Lean checks every step from the spec to the code. It’s the only reliable way I see to ship high-quality code while keeping the speed AI gives you.So the last question is whether this app could be correct by construction.