Lean 4 reaches the top of the $12 Server Challenge
A striking workload-specific result: Lean 4, compiled to C and using io_uring, ties for the leaderboard's top held-user count on a 1-vCPU, 2-GB machine. The shared challenge methodology makes the result more interpretable than an isolated language-performance claim, while still limiting what it says about general-purpose performance.
Harsh Gupta's Lean 4 submission reached the top held-user count in the $12 Server Challenge. The leaderboard reports 280,000 users held for five minutes, 26,683 requests per second, p95 latency of 141 ms, p99 of 316 ms, and 0% errors for lean-derive-hargup, described as Lean 4 compiled to C with io_uring.
This is not a standalone win over every systems language: Mojo and Objective-C also reached 280,000 users, while Rust, C, and handwritten x86-64 assembly entries on this leaderboard held fewer. The challenge is a particular SQLite-backed feed API on a 1-vCPU/2-GB Ubuntu VPS, with a defined interactive load mix and pass thresholds; it is useful evidence about this workload and implementation, not a universal ranking of languages. The organizer documents the test setup and scoring protocol on the leaderboard and the challenge repository.