Vitalik Buterin propone un lenguaje para hacer más legibles las pruebas generadas por IA

Buterin pone el foco en la verificación formal: un lenguaje que haría más legibles para Lean y HOL las pruebas generadas por IA. La propuesta encaja con la hoja de ruta Lean Ethereum y con el desarrollo de una ZK-EVM formalmente verificada.

Puntos clave

• Vitalik Buterin propone un lenguaje de programación que puede compilar directamente a Lean o HOL.
• El objetivo no es acelerar la escritura de pruebas por parte de la IA, sino hacer que el resultado sea más legible y verificable para las personas.
• Buterin todavía no ha presentado un prototipo y mantiene abierta la sintaxis exacta del lenguaje.

El cofundador de Ethereum, Vitalik Buterin, ha planteado un nuevo lenguaje de programación capaz de compilar directamente a Lean o HOL. La idea no busca que la IA redacte pruebas con mayor rapidez, sino que las afirmaciones resultantes sean más fáciles de leer y de verificar para las personas.

Por qué Lean es importante aquí

Lean es un proof assistant que permite a matemáticos e ingenieros comprobar demostraciones paso a paso con ayuda de un ordenador. Aunque la herramienta existe desde hace décadas, durante mucho tiempo se mantuvo como una solución de nicho. Hoy, la comunidad de Lean ya acumula más de 210.000 teoremas y 100.000 definiciones en mathlib, lo que la convierte en una base amplia para las matemáticas formales.

Buterin apunta a un problema muy concreto: la IA ya es capaz de generar grandes bloques de pruebas automatizadas, a menudo más deprisa de lo que podría hacerlo un equipo humano de forma manual. Sin embargo, para un lector resulta difícil identificar con rapidez qué demuestra realmente ese tipo de prueba. En su planteamiento, la lógica interna solo necesita ser correcta desde el punto de vista matemático, mientras que las definiciones y los teoremas están pensados precisamente para ser leídos por personas.

El momento también encaja con el proceso de reconstrucción de Ethereum, conocido como la hoja de ruta Lean Ethereum. En ese marco, además, se está desarrollando una ZK-EVM formalmente verificada, es decir, una versión de conocimiento cero de la Ethereum Virtual Machine, con métodos similares.

La IA escribe, las personas verifican

Buterin cita, entre otros, a Claude, DeepSeek 4 Pro y Leanstral como modelos que ya pueden generar pruebas en Lean. Su propuesta se inserta en una tendencia más amplia, en la que la IA gana peso como apoyo para la verificación formal. En 2025, ACM SIGPLAN reconoció el impacto de Lean en matemáticas, verificación de hardware y software e IA con un premio de software para varios desarrolladores clave del proyecto.

El alcance de esta tecnología va más allá de Ethereum. La verificación formal también se utiliza para respaldar la corrección de sistemas críticos, desde protocolos criptográficos hasta dispositivos médicos. Para los desarrolladores de cripto, un lenguaje más legible puede facilitar la auditoría de afirmaciones sin necesidad de revisar toda la maquinaria de la prueba.

Qué significa para los desarrolladores de Ethereum

Para los lectores europeos de cripto, este avance resulta especialmente relevante porque la verificación formal gana peso en infraestructuras en las que un error puede afectar directamente al dinero o a la seguridad. Ethereum, los sistemas ZK y el código criptográfico son precisamente ámbitos en los que un fallo menor puede tener consecuencias importantes. Por eso, un lenguaje que haga más legible la salida de la IA puede ser valioso como pieza para un software más fiable, no como producto final en sí mismo.

Buterin todavía no ha mostrado un prototipo y dejó abierta la sintaxis exacta. En consecuencia, aún no está claro si los desarrolladores acabarán adoptando un único estándar o si convivirán varias variantes en paralelo.