INSIGHT : Vitalik Buterin propose un nouveau type de langage de programmation. Un langage qui compile vers des systèmes de preuves comme Lean, conçu uniquement pour rendre les définitions et les théorèmes au maximum lisibles par les humains.

Le raisonnement inverse le goulot d’étranglement habituel. « Tout ce qui compte avec les preuves, c’est que les preuves soient correctes. » Les machines vérifient cette partie. Ce dont les humains ont besoin, c’est de comprendre « quelles sont les affirmations exactes et précises qui ont été prouvées ».
Les prouveurs d’IA passent déjà par Lean. AlphaProof, DeepSeek-Prover et Leanstral de Mistral l’utilisent tous comme backend formel, AWS vérifie formellement sa langue d’autorisation, et Microsoft vérifie la cryptographie de production avec.
Récemment, dix agents d’IA ont construit, en un week-end, un langage vérifié avec des optimisations prouvées, sans aucune ligne écrite par des humains. Les preuves arrivent désormais plus vite que quiconque ne peut lire ce qu’elles prétendent.
@VitalikButerin pousse la vérification formelle depuis des années comme réponse aux exploits de smart contracts, et la Fondation Ethereum mène un effort de vérification dédié.
Une couche de théorèmes lisible par les humains manque à ce programme ; les auditeurs pourraient enfin lire ce que garantit réellement un contrat vérifié par une IA.