El demostrador de teoremas Lean ha sido galardonado con el «SIGPLAN Programming Languages Software Award 2025», otorgado por ACM SIGPLAN (Special Interest Group on Programming Languages de la ACM (Association for Computing Machinery).

La cita del premio destaca lo siguiente:

El demostrador de teoremas Lean constituye un sistema informático extraordinario. Fundamentado en sólidas bases teóricas y de ingeniería, Lean ha ejercido y continúa ejerciendo un amplio impacto tanto en la práctica industrial como en la investigación científica.

El proyecto Lean ha generado un impacto particularmente significativo en tres áreas clave: matemáticas, verificación de hardware y software, e inteligencia artificial. En el ámbito matemático, ha logrado una aceptación considerable dentro de la comunidad académica, evidenciada por el desarrollo de Mathlib, una biblioteca creada por usuarios que supera las 1.8 millones de líneas de código.

La credibilidad del sistema se ha consolidado mediante la verificación exitosa de resultados fundamentales, incluyendo Liquid Tensor Experiment (propuesto por el medallista Fields Peter Scholze) y la verificación de la conjetura polinomial de Freiman-Ruzsa dirigida por el medallista Fields Terence Tao. Estos logros han proporcionado al sistema un reconocimiento sin precedentes en la comunidad científica internacional.

Es indiscutible que los métodos formales basados en Lean ocuparán una posición central en el desarrollo de las matemáticas durante los próximos años. Paralelamente, el sistema ha demostrado su valor práctico en proyectos industriales de verificación críticos, tales como la verificación del lenguaje de control de acceso Cedar en Amazon Web Services, la validación del muestreador SampCert para privacidad diferencial (también en AWS), y diversos proyectos de verificación blockchain en empresas líderes como StarkWare y Nethermind.

Finalmente, el éxito de iniciativas como AlphaProof de DeepMind y la adopción estratégica de Lean por parte de empresas emergentes como Harmonic han consolidado su posición como la solución de referencia para sistemas de razonamiento matemático potenciados por inteligencia artificial.