Selon TechFlow, le 21 juillet, Vitalik Buterin (@VitalikButerin) a indiqué dans un post qu'il suggère de développer un nouveau type de langage de programmation de haut niveau, qui peut être compilé en Lean (ou des outils de vérification formelle comme HOL), avec pour objectif principal de permettre aux humains de lire aussi facilement que possible les définitions et le contenu des théorèmes (plutôt que les preuves elles-mêmes). Le scénario d'utilisation envisagé est le suivant : l'IA est responsable de générer le contenu des preuves, tandis que ce langage aide les lecteurs à comprendre rapidement les propositions spécifiques prouvées par l'IA.
Ajouter aux favoris
Partager sur les réseaux sociaux
