Vitalik Buterin, el cerebro detrás de Ethereum, lanzó una propuesta que está dando de qué hablar en los círculos tecnológicos: crear un lenguaje de programación especialmente diseñado para compilar en Lean, una plataforma de verificación matemática formal. El objetivo es simple pero poderoso — que cualquier persona pueda revisar y entender las demostraciones que produce la inteligencia artificial, sin tener que ser un científico de datos ni un matemático de élite.
La preocupación de Buterin no es menor. A medida que los sistemas de IA toman decisiones cada vez más complejas, crece también la tendencia a aceptarlas sin cuestionarlas. Esta propuesta busca romper ese ciclo de confianza ciega, poniendo herramientas de auditoría reales en manos del usuario común.
Para Colombia y el resto de Latinoamérica, donde todavía estamos construyendo bases sólidas de alfabetización digital, esta idea llega en buen momento. Si se materializa, podría cambiar radicalmente la relación que tenemos con la IA — pasando de simples consumidores a personas capaces de exigirle cuentas a la tecnología que usamos todos los días.