Le cofondateur d'Ethereum, Vitalik Buterin, a proposé le développement d'un nouveau langage de programmation de haut niveau visant à améliorer la lisibilité des preuves générées par l'IA. Ce langage serait compilé vers des systèmes de démonstration de théorèmes tels que Lean et HOL, en se concentrant sur la compréhension des « définitions et théorèmes » plutôt que sur le processus de preuve lui-même. L'objectif est de permettre aux humains de comprendre clairement ce que les preuves générées par l'IA ont formellement établi, facilitant ainsi l'examen et la vérification des affirmations mathématiques et logiques.