El cofundador de Ethereum, Vitalik Buterin, ha sugerido el desarrollo de un nuevo lenguaje de programación de alto nivel destinado a mejorar la legibilidad de las pruebas generadas por IA. Este lenguaje se compilaría en sistemas de demostración de teoremas como Lean y HOL, enfocándose en hacer que las "definiciones y teoremas" sean más comprensibles, en lugar del proceso de demostración en sí. El objetivo es permitir que los humanos comprendan claramente lo que las pruebas generadas por IA han establecido formalmente, facilitando un examen y verificación más sencillos de las afirmaciones matemáticas y lógicas.