Hoje (21 de julho), o cofundador do Ethereum Vitalik Buterin propôs a criação de uma nova linguagem de programação de alto nível, capaz de ser compilada para sistemas de demonstração formal como Lean e HOL, a fim de otimizar a legibilidade das definições e dos teoremas — em vez do próprio processo de prova. Segundo o PANews, Buterin disse que essa linguagem foi projetada para ajudar os humanos a entenderem com clareza o que as grandes provas formais geradas por IA expressam em termos de matemática e lógica, permitindo que os leitores verifiquem e validem com mais facilidade as afirmações específicas feitas pela IA.