Lean 4 RealWorld app passes both test suites, mostly written by Claude Code

The author set out to answer a simple question: can you build a real web app in Lean 4 yet? Lean is a functional language in the same family as Haskell and OCaml, best known as a proof assistant, whose standard library has lately gained an HTTP server. To test it, the author built RealWorld, a well-known reference app (a Medium clone) that ships with official test suites for its API and its website. The version here is written entirely in Lean, frontend included, using datastar-lean for interactivity. The code is on GitHub. The post is styled like a math paper, with only the few things actually proved marked as propositions, which Lean checks on every build.

Existence. The author defines a RealWorld implementation as a program that passes the API suite and the website suite, and the proof of the theorem that one exists in Lean is simply to build it and run both suites; they pass. The server is Lean's standard-library Std.Http, available since April. On top of it, lean-routing declares the API routes in a table, with typed path parameters and one handler per route. A sample handler deletes a comment: it checks the login token, calls a service layer and replies 204 No Content. The website calls the same service layer, so it follows the same rules. Other libraries cover JSON (lean-json), password hashing with OpenSSL's scrypt (lean-libcrypto), login tokens (lean-jose), and CORS, cookies and static files (lean-middleware). Data lives in Postgres through leanpostgres, which wraps Postgres's C client and keeps a connection pool. SQL is written inline with sql!, and interpolated values like {email} become query parameters sent separately, so user input cannot run as SQL. leanmigrate applies the schema at server start. Pages are rendered on the server with lean-html, with no templates: the HTML is ordinary Lean functions. Datastar, a small script on the page, sends the DELETE request when a user clicks the trash icon and updates the page with the server's reply, built by the same function the JSON API uses. There is no frontend build step. The author and Carlo Hamalainen maintain datastar-lean, the official Lean SDK for Datastar.

On cost, the Lean backend is 1,033 lines, the shortest of the four implementations the author compared: TypeScript has 1,267 lines, Go 1,371 and C# 2,396. Ten of the eleven libraries it uses are by Paul Butcher, and Claude Code and the author contributed fixes to six of them along the way.

Production. Passing tests on a laptop is not readiness, so the second question is whether it can serve real users. Two problems are named. First, Lean's HTTP server maxes out at a few thousand requests per second per process, mostly because of a bug in Lean's runtime that is already fixed but not yet released. Second, Lean ships a new version every month and new versions often break libraries. The author says neither matters for a small site that pins its versions. A separate issue is who wrote the code: almost none of it was written by hand. Claude Code wrote the app at the author's direction, and most of the libraries were written the same way. It is all a few months old and most of it has one or two contributors, so the bugs found only in real use are probably still in there.

The easiest parts to trust are the types and theorems, because Lean checks them whoever wrote the code. The instructions the libraries give their AI agent ask for the strongest form a claim admits, a proven theorem over a property over an example and an expected result, and forbid using sorry as a placeholder for a missing proof. Several libraries include real proofs. Code no theorem covers is only as reliable as its tests, and that goes double for bindings to C libraries, where Lean cannot check the C code. Proofs still need reading, since Lean checks that a proof is correct but not that the theorem states what you need. 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, and those proofs did not make the code more correct. The author mentions claimcheck, a tool in which an AI model restates each theorem in plain English without knowing its intended meaning, and a second step compares that with the original intent. It is useful but does not replace reading.

The partial answer: yes, the app can serve real users as long as three things hold. (H1) traffic stays modest, (H2) the toolchain is pinned, and (H3) someone actually reads the code. Because the app keeps no state between requests, several copies can be run for more load. At about 1,600 lines in total, reading is feasible, and the author says someone should read its handlers, its SQL and its C bindings carefully before real users see them.

Correctness. The author argues that correctness by construction is the right aim, especially when an AI writes most of the code: write down exactly what the program should do in a formal language, then derive the code in steps each proved correct. Tests only check the cases someone thought to write, Dan Luu's experiments suggest agents write poor tests even when told which technique to use, and a spec alone cannot show the code follows it. Applied to RealWorld, the verdict is that full correctness by construction was not possible. The contract is an OpenAPI file plus the test suites; the OpenAPI file is precise about shapes (endpoints, fields, status codes) but behavior is described only in English and pinned down by tests only for the cases they check. So the author wrote the app first and tested it afterwards, the opposite of the definition, and picked a few important properties to verify instead. Three are guaranteed just by compiling. The first, Proposition 1, is that a handler whose types do not match its route does not compile: lean-routing derives each handler's type from its route, so a handler taking a comment id as a String instead of a Nat fails with a type mismatch error at compile time. The author contrasts this with Express or Go, where each handler parses the id itself, and Rust's axum, where a mismatch only shows when a request arrives. One weak spot remains: the route table was copied from the OpenAPI file by hand, and generating it automatically would close that gap.

The post then shows the idea on a small scale with URL slugs. RealWorld does not say what a slug looks like, so the author wrote the specification first as a Lean type called Valid: a single lowercase letter or digit is valid; a valid slug can be extended by a letter or digit in front, or by a letter or digit followed by a hyphen; nothing else is valid. That rules out empty slugs, hyphens at either end and double hyphens. A Slug is a string bundled with a proof that it follows these rules.

Key facts

• The RealWorld reference app (a Medium clone with official API and website test suites) was built entirely in Lean 4, frontend included, and the author reports that both suites pass.
• The Lean backend is 1,033 lines, the shortest of four implementations compared; TypeScript has 1,267 lines, Go 1,371 and C# 2,396.
• Almost none of the code was written by hand: Claude Code wrote the app at the author's direction, and most of the eleven libraries it uses were written the same way.
• The author says it can serve real users if traffic stays modest, the toolchain is pinned and someone reads the code; the Lean HTTP server tops out at a few thousand requests per second per process.
• Full correctness by construction was not possible because RealWorld is formal only about types; the compiler does guarantee that a handler whose types do not match its route does not compile.

Why it matters

Lean is usually seen as a proof assistant. This project is a concrete test of whether it can carry an ordinary web app: HTTP server, Postgres, password hashing, login tokens and server-rendered pages. The result is compact, at 1,033 backend lines against 1,267 for TypeScript, 1,371 for Go and 2,396 for C#. It also shows a workflow in which an AI agent writes nearly all the code while the type checker and proofs provide the guarantees a reader can rely on.

Who it affects

Developers curious about Lean as an application language, and people who maintain or depend on its young library ecosystem; ten of the eleven libraries used are by Paul Butcher. It also speaks to anyone letting coding agents write production code and wondering what to trust, since the author argues that types and checked theorems hold no matter who or what wrote the code, while everything else is only as reliable as its tests.

How to use it

The code is on GitHub, and the post names the building blocks: Std.Http, lean-routing, lean-json, lean-libcrypto, lean-jose, lean-middleware, leanpostgres, leanmigrate, lean-html and datastar-lean. For anyone deploying something similar, the author's conditions are to keep traffic modest, pin the Lean toolchain, run several copies of the stateless app if more load is needed, and have someone carefully read the handlers, the SQL and the C bindings before real users arrive.

How solid is it

The claims are the author's own: that both RealWorld suites pass, and the line-count comparison. The post gives no test counts beyond that, and no measured benchmark for the server beyond the qualitative few thousand requests per second per process. The text available for this summary stops after the Slug definition in the correctness section, so the rest of that section is not covered. The source does not say the app is deployed in production or has real users.

Risks and caveats

The author is direct about the weak points. The stack is young: Lean releases monthly and new versions often break libraries. The code is a few months old, mostly has one or two contributors, and was written fast by an agent, so bugs that only show in real use are probably still there. Bindings to C libraries cannot be checked by Lean at all. Proofs can also be beside the point: in Dan Luu's Zstd experiment, agents mostly proved arithmetic facts that missed the bug-prone code. The app was not derived from a formal spec, and the route table was copied from the OpenAPI file by hand.

“Yes, as long as three things hold: (H1) traffic stays modest, (H2) you pin the toolchain, and (H3) someone actually reads the code.”

— The post's author, on whether the app can serve real users