Vitalik Buterin quer tornar legíveis as provas geradas por IA com nova linguagem

Buterin centra-se na verificação formal: uma linguagem que torna as provas geradas por IA mais legíveis para Lean e HOL. Isto está alinhado com a Lean roadmap da Ethereum e com o desenvolvimento de uma ZK-EVM formalmente verificada.

Pontos principais

• Vitalik Buterin propõe uma linguagem de programação que pode compilar diretamente para Lean ou HOL.
• O objetivo é tornar as provas de IA mais legíveis e verificáveis para humanos, não fazer com que a IA escreva mais depressa.
• Buterin ainda não mostrou um protótipo e deixou em aberto a sintaxe exacta da linguagem.

O cofundador da Ethereum, Vitalik Buterin apresentou uma proposta para uma nova linguagem de programação capaz de compilar diretamente para Lean ou HOL. A ideia não passa por acelerar a produção de provas por parte da IA, mas sim por tornar essas demonstrações mais claras e fáceis de verificar por pessoas.

Porque é que o Lean aqui conta

Lean é um proof assistant que permite a matemáticos e engenheiros verificar provas passo a passo com o apoio de um computador. Apesar de existir há décadas, manteve-se durante muito tempo num nicho. Ainda assim, a comunidade Lean já ultrapassou os 210.000 teoremas e as 100.000 definições em mathlib, o que faz deste sistema uma base ampla para a matemática formal.

Buterin chama a atenção para um problema prático: a IA já consegue gerar grandes blocos de provas automatizadas, muitas vezes mais depressa do que uma equipa humana conseguiria fazê-lo manualmente. Para quem lê, porém, continua a ser difícil perceber de imediato o que essas provas demonstram na prática. Na sua perspetiva, a lógica interna de uma prova só tem de estar matematicamente correta, enquanto as definições e os teoremas devem permanecer legíveis para pessoas.

Este momento coincide com o próprio processo de reconstrução da Ethereum, também conhecido como a Lean Ethereum roadmap. Nesse trabalho, está também a ser desenvolvida uma ZK-EVM formalmente verificada, uma versão de zero-knowledge da Ethereum Virtual Machine, com métodos semelhantes.

A IA escreve, as pessoas verificam

Buterin menciona, entre outros, Claude, DeepSeek 4 Pro e Leanstral como modelos que já conseguem gerar provas em Lean. Esta evolução insere-se numa tendência mais ampla, na qual a IA é cada vez mais usada na verificação formal. Em 2025, a ACM SIGPLAN reconheceu o impacto do Lean na matemática, na verificação de hardware e software e na IA com um prémio de software atribuído a vários dos principais programadores do projeto.

A importância deste avanço vai além da Ethereum. A verificação formal também serve para sustentar a correção de sistemas críticos, desde protocolos criptográficos até dispositivos médicos. Para os programadores de criptomoedas, uma linguagem mais legível pode facilitar a auditoria de afirmações sem obrigar a percorrer toda a maquinaria das provas.

Significado para os programadores da Ethereum

Para os leitores europeus de criptomoedas, este tema é particularmente relevante porque a verificação formal está a ganhar peso em infraestrutura onde os erros podem afetar diretamente o dinheiro ou a segurança. Ethereum, sistemas ZK e código criptográfico são precisamente os contextos em que um pequeno erro pode ter consequências significativas. Uma linguagem que torne a saída da IA mais legível pode, por isso, revelar-se especialmente útil como bloco de construção para software mais fiável, e não como produto final em si.

Buterin ainda não mostrou um protótipo e deixou em aberto a sintaxe exacta. Por isso, continua por esclarecer se os programadores acabarão por adotar um único padrão ou se trabalharão com várias variantes em paralelo.