O cofundador da Ethereum, Vitalik Buterin, sugeriu o desenvolvimento de uma nova linguagem de programação de alto nível com o objetivo de melhorar a legibilidade das provas geradas por IA. Essa linguagem seria compilada para sistemas de demonstração de teoremas como Lean e HOL, focando em tornar "definições e teoremas" mais compreensíveis, em vez do processo de prova em si. O objetivo é permitir que os humanos compreendam claramente o que as provas geradas por IA estabeleceram formalmente, facilitando o exame e a verificação de reivindicações matemáticas e lógicas.