Lean 4 Can Now Build Real Web Apps, and This One Passes Every Test
I built the RealWorld app in Lean 4
Lean 4 is known as a proof assistant, but its standard library now includes an HTTP server and a growing ecosystem of libraries. I built the full RealWorld app — a Medium clone with API and website test suites — entirely in Lean, including the frontend, using Datastar for interactivity. The backend is only 1,033 lines, the shortest of four implementations compared. It passes both official test suites, though production readiness depends on modest traffic, pinned toolchains, and careful code review.
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 intent. It’s a useful check, but it doesn’t replace reading.
- hiAndrewQuinn
This is terrific news. Last year I looked into Lean for generalist software development and found it was lacking quite a bit in the library department, so the news of e.g. leanpostgres being workable is a huge step forward.
- saviorand
I wanted to know if Lean 4 is usable for an everyday web app yet, not just for proofs, so I built RealWorld (the Medium clone) in it, frontend included, using Datastar. Looks like it's feasible now with the new libraries. This post describes the experience
- solomonb
The secret of Lean4 is that its actually a great programming language, sort like a super Haskell. In fact I like it more as a programming language then as a proof checker!
Dependent types are awesome for regular programming in addition to formal verification. For proof checking I actually prefer Agda.