Gwern Branwen ha publicado una propuesta de investigación titulada 'Lean Software Scaling Laws' que plantea medir empíricamente cómo escala la perplejidad de los modelos de lenguaje grandes (LLM) de programación en función del tamaño del código fuente, tomando Lean como caso de estudio. La hipótesis central es que los lenguajes con mejores exponentes en sus leyes de escalado de 'predecibilidad' terminarán siendo más fáciles de comprender, corregir y producir para los LLM, lo que se traduciría en ganancias reales de seguridad y corrección del software a escala global.
El texto parte de la observación de que los LLM rinden mejor en lenguajes populares como Python por la abundancia de datos de entrenamiento, pero advierte que esa ventaja inicial no implica que el rendimiento se mantenga cuando los codebases crecen y salen de la ventana de contexto. A medida que una base de código se vuelve más compleja, antigua e interconectada, los trucos como monkey-patching, las excepciones, los tipos dinámicos y las dependencias cambiantes vuelven el comportamiento cada vez más impredecible, hasta el punto de que un solo error puede obligar a programadores humanos a dedicar semanas a depurar.
Frente a ese 'fracaso de escala', el autor propone Lean como el caso extremo más prometedor: un lenguaje con disciplina de tipos fuerte, seguridad de memoria y potencia expresiva capaz de soportar programas grandes. Reconoce que los LLM de 2026 parten con una constante base peor y mayor pérdida total sobre Lean por la escasez de código de entrenamiento, pero sostiene que su exponente de escalado podría ser mejor, de modo que, con suficiente volumen, las implementaciones en Lean terminarían superando a las de lenguajes dinámicos y aportarían beneficios como la eliminación de errores de memoria y la demostración formal de propiedades críticas como la compresión sin pérdidas.
El artículo describe la metodología para validar la hipótesis: medir perplejidad sobre ventanas de contexto crecientes en modelos contemporáneos, una vía barata comparada con entrenar desde cero. También discute los riesgos: que Lean resulte mal diseñado, que los codebases reales deriven en un 'big ball of mud' o proliferen pruebas ad hoc ('mathslop'), o que la perplejidad aislada no capture realmente la predecibilidad útil. La investigación pretende, en definitiva, decidir si conviene invertir a gran escala en reescribir software en Lean para mejorar la ciberseguridad mundial.