Vitalik Buterin veut rendre les preuves IA plus lisibles avec un nouveau langage
Buterin met l’accent sur la vérification formelle avec un langage conçu pour rendre les preuves générées par IA plus lisibles dans Lean et HOL. Cette approche s’inscrit dans la feuille de route Lean Ethereum et dans le développement d’une ZK-EVM formellement vérifiée.
À retenir
- Vitalik Buterin propose un langage de programmation capable de compiler directement vers Lean ou HOL.
- L’idée est de rendre les preuves produites par l’IA plus lisibles et plus simples à vérifier pour des humains, et non d’accélérer l’écriture de preuves par l’IA.
- Buterin n’a pas encore montré de prototype et la syntaxe exacte du langage reste à définir.
Le cofondateur d’Ethereum, Vitalik Buterin, a présenté un nouveau langage de programmation pensé pour compiler directement vers Lean ou HOL. Son objectif n’est pas de laisser l’IA produire des proofs plus vite, mais de rendre ces démonstrations plus lisibles et plus faciles à contrôler par des humains.
Pourquoi Lean est central dans cette approche
Lean est un assistant de preuve qui permet aux mathématiciens et aux ingénieurs de faire vérifier des démonstrations, étape par étape, par un ordinateur. L’outil existe depuis longtemps, mais il est resté cantonné à un usage de niche. La communauté Lean a désormais répertorié plus de 210 000 théorèmes et 100 000 définitions dans mathlib, ce qui en fait une base particulièrement riche pour les mathématiques formelles.
Buterin pointe surtout un problème très concret : l’IA sait désormais générer d’importants blocs de proofs automatisées, souvent bien plus rapidement qu’une équipe humaine. Pour un lecteur, en revanche, il reste difficile de comprendre d’un coup d’œil ce qu’une proof établit réellement. Selon lui, la logique interne d’une proof doit avant tout être correcte sur le plan mathématique, tandis que les définitions et les théorèmes doivent rester lisibles pour des humains.
Ce travail s’inscrit dans le chantier de refonte d’Ethereum, aussi connu sous le nom de feuille de route Lean Ethereum. Dans ce cadre, les équipes travaillent également sur une ZK-EVM formellement vérifiée, c’est-à-dire une version zero knowledge de l’Ethereum Virtual Machine, avec des méthodes proches.
L’IA produit, les humains valident
Buterin cite notamment Claude, DeepSeek 4 Pro et Leanstral parmi les modèles déjà capables de générer des proofs Lean. Cette évolution s’inscrit dans une tendance plus large, où l’IA prend une place croissante dans la vérification formelle. En 2025, ACM SIGPLAN a d’ailleurs salué l’impact de Lean sur les mathématiques, la vérification du matériel et des logiciels, ainsi que sur l’IA, en attribuant un software award à plusieurs développeurs clés du projet.
Les implications dépassent largement Ethereum. La vérification formelle sert aussi à démontrer la fiabilité de systèmes critiques, qu’il s’agisse de protocoles cryptographiques ou de dispositifs médicaux. Pour les développeurs crypto, un langage plus lisible peut donc faciliter l’audit d’affirmations techniques sans devoir passer en revue toute la mécanique des proofs.
Ce que cela change pour les développeurs Ethereum
Pour les lecteurs européens de la crypto, l’enjeu est surtout là : la vérification formelle prend une place de plus en plus importante dans les infrastructures où la moindre erreur peut avoir un impact direct sur l’argent ou la sécurité. Ethereum, les systèmes ZK et le code cryptographique font précisément partie des domaines où une petite faille peut avoir de lourdes conséquences. Un langage qui rend la sortie de l’IA plus lisible peut donc surtout servir de brique pour un logiciel plus fiable, plutôt que de produit final à lui seul.
Buterin n’a pas encore présenté de prototype et la syntaxe exacte du langage reste ouverte. Il est donc encore impossible de savoir si les développeurs convergeront vers une norme unique ou s’ils feront coexister plusieurs variantes.
