Lean 4 ya puede construir una app web real: el experimento RealWorld
I built the RealWorld app in Lean 4
Un desarrollador construyó la app de referencia RealWorld completamente en Lean 4, incluyendo frontend con datastar-lean, y pasó las suites de pruebas oficiales. El backend ocupa 1,033 líneas, menos que las versiones en TypeScript, Go y C#. Aunque el stack es joven y el servidor HTTP tiene límites, el autor concluye que puede servir usuarios reales si el tráfico es moderado, se fija la toolchain y alguien revisa el código.
Casi nada de este código fue escrito a mano. Claude Code escribió la aplicación bajo mi dirección. La mayoría de las librerías fueron escritas de la misma manera. Todo tiene unos meses de antigüedad. La mayor parte solo tiene uno o dos contribuidores.